| apply (trans s)]]
qed.
-(* questa coercion e' necessaria per problemi di unificazione *)
coercion setoid1_of_setoid.
+prefer coercion Type_OF_setoid.
definition reflexive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x.
definition symmetric2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x.
| apply (trans1 s)]]
qed.
-(*coercion setoid2_of_setoid1.*)
-
-(*
-definition Leibniz: Type → setoid.
- intro;
- constructor 1;
- [ apply T
- | constructor 1;
- [ apply (λx,y:T.cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y)
- | alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
- apply refl_eq
- | alias id "sym_eq" = "cic:/matita/logic/equality/sym_eq.con".
- apply sym_eq
- | alias id "trans_eq" = "cic:/matita/logic/equality/trans_eq.con".
- apply trans_eq ]]
-qed.
-
-coercion Leibniz.
-*)
+coercion setoid2_of_setoid1.
+prefer coercion Type_OF_setoid2.
+prefer coercion Type_OF_setoid.
+prefer coercion Type_OF_setoid1.
+(* we prefer 0 < 1 < 2 *)
interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
qed.
alias symbol "eq" = "setoid1 eq".
-definition if': ∀A,B:CPROP. A = B → A → B.
- intros; apply (if ?? e); assumption.
+definition fi': ∀A,B:CPROP. A = B → B → A.
+ intros; apply (fi ?? e); assumption.
qed.
-notation ". r" with precedence 50 for @{'if $r}.
-interpretation "if" 'if r = (if' __ r).
+notation ". r" with precedence 50 for @{'fi $r}.
+interpretation "fi" 'fi r = (fi' __ r).
definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
constructor 1;
| apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
qed.
-(*
-definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
- intro;
- constructor 1;
- [ apply (eq_rel ? (eq S))
- | intros; split; intro;
- [ apply (.= H \sup -1);
- apply (.= H2);
- assumption
- | apply (.= H);
- apply (.= H2);
- apply (H1 \sup -1)]]
-qed.
-*)
-
record category : Type1 ≝
{ objs:> Type0;
arrows: objs → objs → setoid;
interpretation "category composition" 'compose x y = (fun2 ___ (comp ____) y x).
interpretation "category assoc" 'assoc = (comp_assoc ________).
-(* bug grande come una casa?
- Ma come fa a passare la quantificazione larga??? *)
-definition unary_morphism_setoid: setoid → setoid → setoid1.
+definition unary_morphism_setoid: setoid → setoid → setoid.
intros;
constructor 1;
[ apply (unary_morphism s s1);
intros; apply o; qed.
coercion setoid_of_SET.
-definition setoid1_of_SET: SET → setoid1.
- intro; whd in t; apply setoid1_of_setoid; apply t.
-qed.
-coercion setoid1_of_SET.
-
-definition eq': ∀w:SET.equivalence_relation ? := λw.eq w.
-
-definition prop1_SET :
- ∀A,B:SET.∀w:arrows1 SET A B.∀a,b:Type_OF_objs1 A.eq' ? a b→eq' ? (w a) (w b).
-intros; apply (prop1 A B w a b e);
-qed.
-
-
-interpretation "SET dagger" 'prop1 h = (prop1_SET _ _ _ _ _ h).
notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
-interpretation "SET eq" 'eq x y = (eq_rel _ (eq' _) x y).
-definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2.
+definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
intros;
constructor 1;
[ apply (unary_morphism1 s s1);
intros; apply o; qed.
coercion setoid1_OF_SET1.
-
-definition eq'': ∀w:SET1.equivalence_relation1 ? := λw.eq1 w.
-
-definition prop11_SET1 :
- ∀A,B:SET1.∀w:arrows2 SET1 A B.∀a,b:Type_OF_objs2 A.eq'' ? a b→eq'' ? (w a) (w b).
-intros; apply (prop11 A B w a b e);
-qed.
-
+
definition setoid2_OF_category2: Type_OF_category2 SET1 → setoid2.
intro; apply (setoid2_of_setoid1 t); qed.
coercion setoid2_OF_category2.
coercion Type1_OF_SET1.
definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply setoid1_of_SET; apply U
+ [ apply rule U;
| intros; apply c;]
qed.
coercion Type_OF_setoid1_of_carr.
-interpretation "SET dagger" 'prop1 h = (prop11_SET1 _ _ _ _ _ h).
+definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
+coercion carr'. (* we prefer the lower carrier projection *)
+
interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
-interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y).
lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.
intros; apply t;