...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / r-o-basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 72c5fe02d603608d30a73bbb87ce07e29c119f8b..b3332c15bf0ecf5a5bcb3fedb10a58952412ddab 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -15,7 +15,7 @@
 include "basic_pairs_to_o-basic_pairs.ma".
 include "apply_functor.ma".
 
-definition rOBP ≝ Apply ?? BP_to_OBP.
+definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
 
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
@@ -23,7 +23,39 @@ lemma rOR_full :
   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
     exT22 ? (λg:arrows2 rOBP s t.
        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intro; cases s (s_2 s_1 s_eq); clear s; cases s_eq; clear s_eq s_2;
+intro; cases s (s_2 s_1 s_eq); clear s;
+whd in ⊢ (?→? (? ? (? ?? ? %) ?)→?);
+whd in ⊢ (?→?→? ? (λ_:?.? ? ? (? ? ? (? ? ? (? ? ? ? % ?) ?)) ?));;
+include "logic/equality.ma".
+lapply (
+match s_eq in eq return 
+ (λright_1:?.(λmatched:(eq (objs2 OBP) (map_objs2 (category2_of_category1 BP) OBP BP_to_OBP s_1) right_1).
+  (∀t:(objs2 rOBP).
+   (∀f:(carr2 (arrows2 OBTop (map_objs2 OBP OBTop OR right_1) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))).
+    (exT22 (carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)) 
+     (λg:(carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)).
+      (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) 
+       (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))      
+       (carr1_OF_Ocontinuous_relation 
+         (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP (*XXX*)right_1 s_1 matched))) 
+         (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) 
+         (fun12 
+          (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) 
+          (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) 
+          (map_arrows2 OBP OBTop OR right_1 (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) 
+          (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t g)))
+      ?)))))))
+       with
+       [ refl_eq ⇒ ?
+]);
+    STOP.   
+       (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) 
+        (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))))) 
+        (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (fun12 (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) (map_arrows2 OBP OBTop OR ? (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched) t g))) 
+        (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) f)))))))) with 
+ [ refl_eq ⇒ ?
+]);
+cases s_eq; clear s_eq s_2;
 intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
 intro; whd in s_1 t_1;
@@ -73,8 +105,8 @@ STOP;
 
 3. Definire la funzione
     Apply:
-     \forall C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 -> CAT2
-    :=
+    ∀C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 → CAT2
+    ≝ 
      constructor 1;
       [ gli oggetti sono gli oggetti di C1 mappati da F
       | i morfismi i morfismi di C1 mappati da F
@@ -89,7 +121,7 @@ STOP;
    al punto 5)
 
 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
-  [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
+  [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
 
 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
    quando applicato a rOBP.
@@ -101,7 +133,7 @@ STOP;
 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 
 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
-   basta prendere (OR \circ BP_to_OBP).
+   basta prendere (OR ∘ BP_to_OBP).
 
 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'