|
0
|
1 module moggi where
|
|
|
2
|
|
|
3
|
|
|
4 postulate A : Set
|
|
|
5 postulate A1 : Set
|
|
|
6 postulate A2 : Set
|
|
|
7
|
|
|
8 postulate x : A
|
|
|
9 postulate e1 : A1
|
|
|
10 --postulate f : A1 -> A2
|
|
|
11
|
|
|
12 data _==_ : {A : Set} -> A -> A -> Set where
|
|
|
13 refl : {x : A} -> x == x
|
|
|
14 sym : {x y : A} -> x == y -> y == x
|
|
|
15 trans : {x y z : A} -> x == y -> y == z -> x == z
|
|
|
16 congr : {x y : A1} -> (f : A1 -> A2) -> x == y ->
|
|
|
17 f x == f y
|
|
|
18
|
|
|
19 record Term (A : Set) : Set where
|
|
|
20 field
|
|
|
21 type : A
|
|
|
22 var : A -> (A -> A)
|
|
|
23 f : A1 -> A2
|
|
|
24 eq : (g1 : A1 -> A2) -> (g2 : A1 -> A2) -> g1 == g2
|
|
|
25
|
