--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/moggi.agda	Sun May 11 19:32:45 2014 +0900
@@ -0,0 +1,25 @@
+module moggi where
+
+
+postulate A : Set
+postulate A1 : Set
+postulate A2 : Set
+
+postulate x : A
+postulate e1 : A1
+--postulate f : A1 -> A2
+
+data _==_ : {A : Set} -> A -> A -> Set where
+  refl  : {x : A} -> x == x
+  sym   : {x y : A} -> x == y -> y == x
+  trans : {x y z : A} -> x == y -> y == z -> x == z
+  congr : {x y : A1} -> (f : A1 -> A2) -> x == y -> 
+            f x == f y
+
+record Term (A : Set) : Set where
+  field
+    type : A
+    var  : A -> (A -> A)
+    f    : A1 -> A2
+    eq   : (g1 : A1 -> A2) -> (g2 : A1 -> A2) -> g1 == g2
+