-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.
-
-(*
-record dependent_product (A:setoid) (B: A ⇒ setoids): Type ≝
- { dp:> ∀a:A.carr (B a);
- dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
- }.*)
-
-record forall (A:setoid) (B: A ⇒ CCProp): CProp ≝
- { fo:> ∀a:A.proofs (B a) }.
-
-record subset (A: setoid) : CProp ≝
- { mem: A ⇒ CCProp }.
-
-definition ssubset: setoid → setoid1.
- intro;
- constructor 1;
- [ apply (subset s);
- | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
- | simplify;
- intros;
- split;
- intro;
- assumption
- | simplify;
- cases daemon
- | cases daemon]
-qed.
-
-definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
- intros;
- constructor 1;
- [ apply mem;
- | unfold function_space_setoid1; simplify;
- intros (b b');
- change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
- unfold proofs1; simplify; intros;
- unfold proofs1 in c; simplify in c;
- unfold ssubset in c; simplify in c;
- cases (c a); clear c;
- split;
- assumption]
-qed.
-
-(*
-definition sand: CCProp ⇒ CCProp.
+nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝
+ { fun2:2> A → B → C;
+ prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
+ }.