-definition function_space_setoid: setoid → setoid → setoid.
- intros (A B);
- constructor 1;
- [ apply (function_space A B);
- | intros;
- apply (∀a:A. proofs (eq ? (f a) (f1 a)));
- | simplify;
- intros;
- apply (f_ok ? ? x);
- unfold carr; unfold proofs; simplify;
- apply (refl A)
- | simplify;
- intros;
- unfold carr; unfold proofs; simplify;
- apply (sym B);
- apply (f a)
- | simplify;
- intros;
- unfold carr; unfold proofs; simplify;
- apply (trans B ? (y a));
- [ apply (f a)
- | apply (f1 a)]]
-qed.
-
-definition function_space_setoid1: setoid1 → setoid1 → setoid1.
- intros (A B);
- constructor 1;
- [ apply (function_space1 A B);
- | intros;
- apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
- |*: cases daemon] (* simplify;
- intros;
- apply (f1_ok ? ? x);
- unfold proofs; simplify;
- apply (refl1 A)
- | simplify;
- intros;
- unfold proofs; simplify;
- apply (sym1 B);
- apply (f a)
- | simplify;
- intros;
- unfold carr; unfold proofs; simplify;
- apply (trans1 B ? (y a));
- [ apply (f a)
- | apply (f1 a)]] *)
-qed.
-
-interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
-
-record isomorphism (A,B: setoid): Type ≝
- { map1:> function_space_setoid A B;
- map2:> function_space_setoid B A;
- inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
- inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
- }.
-
-interpretation "isomorphism" 'iff x y = (isomorphism x y).
-
-definition setoids: setoid1.
- constructor 1;
- [ apply setoid;
- | apply isomorphism;
- | intro;
- split;
- [1,2: constructor 1;
- [1,3: intro; assumption;
- |*: intros; assumption]
- |3,4:
- intros;
- simplify;
- unfold proofs; simplify;
- apply refl;]
- |*: cases daemon]
-qed.
-
-definition setoid1_of_setoid: setoid → setoid1.
- intro;
- constructor 1;
- [ apply (carr s)
- | apply (eq s)
- | apply (refl s)
- | apply (sym s)
- | apply (trans s)]
-qed.
-
-coercion setoid1_of_setoid.
+notation "† c" with precedence 90 for @{'prop1 $c }.
+notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
+notation "#" with precedence 90 for @{'refl}.
+interpretation "prop1" 'prop1 c = (prop1 ????? c).
+interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
+interpretation "refl" 'refl = (refl ???).
+
+ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
+#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
+##[ #f; #g; napply (∀x,y. f x y = g x y);
+##| #f; #x; #y; napply #;
+##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
+nqed.