From 6ca487df4f361fd6b0a3b0734396bc6a62b520c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Feb 2009 14:44:47 +0000 Subject: [PATCH] ... --- .../overlap/r-o-basic_pairs.ma | 44 ++++++++++++++++--- 1 file changed, 38 insertions(+), 6 deletions(-) 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 72c5fe02d..b3332c15b 100644 --- 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' -- 2.39.2