Mercurial > hg > Members > atton > agda > moggi

comparison moggi.agda @ 0:530373ccbcee default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define 2.1 table
author atton
date Sun, 11 May 2014 19:32:45 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:530373ccbcee
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