the new coercion behaviour (variants + composition with ID) and the new

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index e22402d9f52542745b29e226597fe74a14920622..c5db6ad6082e91d03461ffba6f3341b924849b0b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -156,6 +156,9 @@ definition CPROP: setoid1.
         [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
 qed.
 
+definition CProp0_of_CPROP: carr1 CPROP → CProp0 ≝ λx.x.
+coercion CProp0_of_CPROP.
+
 alias symbol "eq" = "setoid1 eq".
 definition fi': ∀A,B:CPROP. A = B → B → A.
  intros; apply (fi ?? e); assumption.
@@ -196,11 +199,12 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
      | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
 qed.
 
+
 record category : Type1 ≝
  { objs:> Type0;
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism1 (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
@@ -252,9 +256,9 @@ qed.
 definition SET: category1.
  constructor 1;
   [ apply setoid;
-  | apply rule (λS,T:setoid.unary_morphism_setoid S T);
+  | apply rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T));
   | intros; constructor 1; [ apply (λx:carr o.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
      apply († (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
     apply trans; [ apply (b (a' a1)); | lapply (prop1 ?? b (a a1) (a' a1));
@@ -265,10 +269,13 @@ definition SET: category1.
   ]
 qed.
 
-definition setoid_of_SET: objs1 SET → setoid.
- intros; apply o; qed.
+definition setoid_of_SET: objs1 SET → setoid ≝ λx.x.
 coercion setoid_of_SET.
 
+definition unary_morphism_setoid_of_arrows1_SET: 
+  ∀P,Q.arrows1 SET P Q → unary_morphism_setoid P Q  ≝ λP,Q,x.x.
+coercion unary_morphism_setoid_of_arrows1_SET.
+
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
 
@@ -285,12 +292,16 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
      | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
 qed.
 
+definition unary_morphism1_of_unary_morphism1_setoid1 : 
+  ∀S,T. unary_morphism1_setoid1 S T → unary_morphism1 S T ≝ λP,Q,x.x.
+coercion unary_morphism1_of_unary_morphism1_setoid1.
+
 definition SET1: category2.
  constructor 1;
   [ apply setoid1;
-  | apply rule (λS,T.unary_morphism1_setoid1 S T);
+  | apply rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T));
   | intros; constructor 1; [ apply (λx.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
      apply († (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
     apply trans1; [ apply (b (a' a1)); | lapply (prop11 ?? b (a a1) (a' a1));
@@ -301,36 +312,17 @@ definition SET1: category2.
   ]
 qed.
 
-definition setoid1_OF_SET1: objs2 SET1 → setoid1.
- intros; apply o; qed.
+definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.
+coercion setoid1_of_SET1.
 
-coercion setoid1_OF_SET1.
+definition unary_morphism1_setoid1_of_arrows2_SET1: 
+  ∀P,Q.arrows2 SET1 P Q → unary_morphism1_setoid1 P Q ≝ λP,Q,x.x.
+coercion unary_morphism1_setoid1_of_arrows2_SET1.
  
-definition setoid2_OF_category2: Type_OF_category2 SET1 → setoid2.
- intro; apply (setoid2_of_setoid1 t); qed.
-coercion setoid2_OF_category2.
-
-definition objs2_OF_category1: Type_OF_category1 SET → objs2 SET1.
- intro; apply (setoid1_of_setoid t); qed.
-coercion objs2_OF_category1.
+variant objs2_of_category1: objs1 SET → objs2 SET1 ≝ setoid1_of_setoid.
+coercion objs2_of_category1.
 
-definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1.
- intro; whd in t; apply (carr1 t);
-qed.
-coercion Type1_OF_SET1.
-
-definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply rule U; 
- | intros; apply c;]
-qed.
-coercion Type_OF_setoid1_of_carr.
-
-definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
-coercion carr'. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_objs1.
 
 interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
-
-lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.
- intros; apply t;
-qed.
-coercion unary_morphism1_of_arrows1_SET1.