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