# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1414888889 -32400
# Node ID 36c9175d9adb22c255cd39aeb8692d4c5bb2da5f
# Parent  4c1a6ce23f9ebc34c6ea2df958001559fa0fa4c4
Migrate moggi from atton/agda/moggi (0:530373ccbcee)

diff -r 4c1a6ce23f9e -r 36c9175d9adb moggi/moggi.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/moggi/moggi.agda	Sun Nov 02 09:41:29 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
+