------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how the Record module can be used
------------------------------------------------------------------------

-- Taken from Randy Pollack's paper "Dependently Typed Records in Type
-- Theory".

module README.Record where

open import Data.Product
open import Data.String
open import Function using (flip)
open import Level
import Record
open import Relation.Binary

-- Let us use strings as labels.

open Record String _≟_

-- Partial equivalence relations.

PER : Signature _
PER =  , "S"       _  Set)
        , "R"       r  r · "S"  r · "S"  Set)
        , "sym"     r  Lift (Symmetric (r · "R")))
        , "trans"   r  Lift (Transitive (r · "R")))

-- Given a PER the converse relation is also a PER.

converse : (P : Record PER) 
           Record (PER With "S"   _  P · "S")
                       With "R"   _  flip (P · "R")))
converse P =
  Rec′⇒Rec
    (PER With "S"   _  P · "S")
         With "R"   _  flip (P · "R")))
    ((((_ ,) ,) , lift λ {_}  lower (P · "sym")) ,
     (lift λ {_} yRx zRy  lower (P · "trans") zRy yRx))