minor fixes

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_pairs_to_o-basic_topologies.ma

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 432025c992f1d9558aaf9d6b6fd9a9e319ffc613..bfd76f99e31ed73bd6869051cceb62fd124d0741 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
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "notation.ma".
 include "o-basic_pairs.ma".
 include "o-basic_topologies.ma".
 
@@ -24,7 +25,7 @@ definition o_basic_topology_of_o_basic_pair: OBP → BTop.
   [ apply (Oform t);
   | apply (□_t ∘ Ext⎽t);
   | apply (◊_t ∘ Rest⎽t);
-  | intros 2; split; intro;
+  | apply hide; intros 2; split; intro;
      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
        apply f_minus_star_image_monotone;
@@ -36,7 +37,7 @@ definition o_basic_topology_of_o_basic_pair: OBP → BTop.
         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
           apply (. (or_prop2 : ?) ^ -1);
           apply oa_leq_refl; ]]
-  | intros 2; split; intro;
+  | apply hide; intros 2; split; intro;
      [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
@@ -48,7 +49,7 @@ definition o_basic_topology_of_o_basic_pair: OBP → BTop.
         | change with ((⊩) ((⊩)* V) ≤ V);
           apply (. (or_prop1 : ?));
           apply oa_leq_refl; ]]
-  | intros;
+  | apply hide; intros;
     apply (.= (oa_overlap_sym' : ?));
     change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
@@ -63,7 +64,7 @@ definition o_continuous_relation_of_o_relation_pair:
  intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
-  | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
     apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
@@ -76,7 +77,7 @@ definition o_continuous_relation_of_o_relation_pair:
     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
     apply (†e^-1);
-  | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+  | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
     apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
@@ -91,6 +92,66 @@ definition o_continuous_relation_of_o_relation_pair:
     apply (†e^-1);]
 qed.
 
+
+definition OR : carr3 (arrows3 CAT2 OBP BTop).
+constructor 1;
+[ apply o_basic_topology_of_o_basic_pair;
+| intros; constructor 1;
+  [ apply o_continuous_relation_of_o_relation_pair;
+  | apply hide; 
+    intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
+    change with ((a \sub \f ⎻* ∘ A (o_basic_topology_of_o_basic_pair S)) =
+                 (a' \sub \f ⎻*∘A (o_basic_topology_of_o_basic_pair S)));
+    whd in e; cases e; clear e e2 e3 e4;
+    change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
+    apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
+    change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a\sub\f ∘ ⊩\sub S)⎻*;
+    apply (.= #‡†(Ocommute:?)^-1);
+    apply (.= #‡e1);
+    change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
+    apply (.= #‡†(Ocommute:?));    
+    change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );    
+    apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
+    apply refl2;]
+| intros 2 (o a); apply rule #;
+| intros 6; apply refl1;]
+qed.
+
+(*
+axiom DDD : False.
+
+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)).
+intros; constructor 1;
+    [ intros(F G); apply (\fst F =_2 \fst G);
+    | intro; apply refl2;
+    | intros 3; apply sym2; assumption;
+    | 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;
+  [ 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;
+  | apply sigma_equivalence_relation2;] 
+| intro o; 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;
+  [ 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)))]
+    cases o1; cases x; cases H; 
+
 (* scrivo gli statement qua cosi' verra' un conflitto :-)
 
 1. definire il funtore OR
@@ -105,7 +166,9 @@ qed.
       | i morfismi i morfismi di C1 mappati da F
       | ....
       ]
-
+   
+   E : objs CATS === Σx.∃y. F y = x
+  
    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
@@ -164,3 +227,4 @@ qed.
     con Giovanni
 
 *)
+