1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
------------------------------------------------------------------------
-- 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".
{-# OPTIONS --with-K #-}
module README.Data.Record where
open import Data.Product.Base using (_,_)
open import Data.String
open import Function.Base using (flip)
open import Level
open import Relation.Binary.Definitions using (Symmetric; Transitive)
import Data.Record as Record
-- 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 (_ ,
lift λ {_} → lower (P · "sym")) ,
lift λ {_} yRx zRy → lower (P · "trans") zRy yRx)
|
