...

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index bfd76f99e31ed73bd6869051cceb62fd124d0741..4971b8ef928f72f44215d55cbf85292512420933 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -117,9 +117,12 @@ constructor 1;
 | intros 6; apply refl1;]
 qed.
 
-(*
 axiom DDD : False.
 
+definition Fo := 
+  λC1,C2: CAT2.λF:arrows3 CAT2 C1 C2.
+    (exT22 ? (λx:C2.exT22 ? (λy:C1.map_objs2 ?? F y =_\ID x))).
+    
 definition sigma_equivalence_relation2:
  ∀C2:CAT2.∀Q.∀X,Y:exT22 ? (λy:C2.Q y).∀P. 
    equivalence_relation2 (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).P f)).
@@ -130,23 +133,58 @@ intros; constructor 1;
     | intros 5; apply (trans2 ?? ??? x1 x2);]
 qed.     
 
-definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2.
-intros (C1 C2 F);
-constructor 1; 
-[ apply (exT22 ? (λx:C2.exT22 ? (λy:C1.map_objs2 ?? F y =_\ID x)));
-| intros (X Y); constructor 1;
+lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F.
+  arrows2 C2 (F (\fst (\snd X))) (F (\fst (\snd Y))) → 
+  arrows2 C2 (\fst X) (\fst Y).           
+intros 5; cases X; cases Y; cases x; cases x1; clear X Y x x1; 
+cases H; cases H1; intros; assumption;
+qed.           
+
+definition Fm : 
+ ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.
+   Fo ?? F → Fo ?? F → setoid2. 
+intros (C1 C2 F X Y); constructor 1;
   [ apply (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).
            exT22 ? (λg:arrows2 C1 (\fst (\snd X)) (\fst (\snd Y)). 
-           ? (map_arrows2 ?? F ?? g) = f)));
-    intro; apply hide; clear g f; cases X in c; cases Y; cases x; cases x1; clear X Y x x1;
-    simplify; cases H; cases H1; intros; assumption;
+           REW ?? F  X Y (map_arrows2 ?? F ?? g) = f)));
   | apply sigma_equivalence_relation2;] 
-| intro o; constructor 1; 
-   [ apply (id2 C2 (\fst o))
+qed.
+
+definition F_id : 
+ ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o.Fm ?? F o o.
+intros; constructor 1; 
+   [ apply (id2 C2 (\fst o));
    | exists[apply (id2 C1 (\fst (\snd o)))] 
      cases o; cases x; cases H; unfold hide; simplify;
      apply (respects_id2 ?? F);]
-| intros (o1 o2 o3); constructor 1;
+qed.
+
+definition F_comp : 
+  ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3.
+    binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3).
+intros; constructor 1;
+[ intros (f g); constructor 1;
+    [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g));
+    | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))]
+      cases o1 in f; cases o2 in g; cases o3; clear o1 o2 o3; 
+      cases x; cases x1; cases x2; clear x x1 x2;
+      cases H; cases H1; cases H2; simplify; intros 2;
+      cases c; cases c1; cases x; cases x1; clear x x1 c c1; simplify;
+      apply (.= (respects_comp2:?));
+      apply (x3‡x2);]
+| (* DISABILITARE INNERTYPES *)
+  STOP
+      cases x3; cases x2;
+      apply refl2;
+      simplify;
+
+definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2.
+intros (C1 C2 F);
+constructor 1; 
+[ apply (Fo ?? F);
+| apply (Fm ?? F); 
+| apply F_id; 
+| apply F_comp; intros (o1 o2 o3); constructor 1;
   [ intros (f g); whd in f g; constructor 1;
     [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g));
     | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))]