1. CProp_n fixed to be equal to Type_n to better understand what is happening

[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 86bc2529cda85de608a0ab1087396d277af75efe..67db8176c9673a08ebd57e10f4266414df8063cf 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -31,15 +31,17 @@ coercion Type_OF_Type1.
 coercion Type_OF_Type2.
 coercion Type_OF_Type3.
 
-definition CProp0 := CProp.
-definition CProp1 := CProp.
-definition CProp2 := CProp.
+definition CProp0 := Type0.
+definition CProp1 := Type1.
+definition CProp2 := Type2.
+(*
 definition CProp0_lt_CProp1 := (CProp0 : CProp1).
 definition CProp1_lt_CProp2 := (CProp1 : CProp2).
 
 definition CProp_OF_CProp0: CProp0 → CProp := λx.x.
 definition CProp_OF_CProp1: CProp1 → CProp := λx.x.
 definition CProp_OF_CProp2: CProp2 → CProp := λx.x.
+*)
 
 record equivalence_relation (A:Type0) : Type1 ≝
  { eq_rel:2> A → A → CProp0;
@@ -194,7 +196,7 @@ definition CPROP: setoid1.
      | intros 1; split; intro; assumption
      | intros 3; cases H; split; assumption
      | intros 5; cases H; cases H1; split; intro;
-        [ apply (H4 (H2 x1)) | apply (H3 (H5 z1))]]]
+        [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
 qed.
 
 alias symbol "eq" = "setoid1 eq".
@@ -233,8 +235,8 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
   [ apply (λA,B. A → B)
   | intros; split; intros;
-     [ apply (if ?? e1); apply H; apply (fi ?? e); assumption
-     | apply (fi ?? e1); apply H; apply (if ?? e); assumption]]
+     [ apply (if ?? e1); apply f; apply (fi ?? e); assumption
+     | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
 qed.
 
 (*
@@ -303,8 +305,8 @@ definition unary_morphism_setoid: setoid → setoid → setoid1.
   | constructor 1;
      [ intros (f g); apply (∀a:s. eq ? (f a) (g a));
      | intros 1; simplify; intros; apply refl;
-     | simplify; intros; apply sym; apply H;
-     | simplify; intros; apply trans; [2: apply H; | skip | apply H1]]]
+     | simplify; intros; apply sym; apply f;
+     | simplify; intros; apply trans; [2: apply f; | skip | apply f1]]]
 qed.
 
 definition SET: category1.
@@ -354,8 +356,8 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid2.
        alias symbol "eq" = "setoid1 eq".
        apply (∀a: carr1 s. f a = g a);
      | intros 1; simplify; intros; apply refl1;
-     | simplify; intros; apply sym1; apply H;
-     | simplify; intros; apply trans1; [2: apply H; | skip | apply H1]]]
+     | simplify; intros; apply sym1; apply f;
+     | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
 qed.
 
 definition SET1: category2.