--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "categories.ma".
+include "notation.ma".
+
+record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type2 ≝ {
+ F2: C2;
+ F1: C1;
+ FP: map_objs2 ?? F F1 =_\ID F2
+}.
+
+lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F.
+ arrows2 C2 (F (F1 ??? X)) (F (F1 ??? Y)) →
+ arrows2 C2 (F2 ??? X) (F2 ??? Y).
+intros 5; cases X; cases Y; clear X Y;
+cases H; cases H1; intros; assumption;
+qed.
+
+record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type2 ≝ {
+ Fm2: arrows2 C2 (F2 ??? X) (F2 ??? Y);
+ Fm1: arrows2 C1 (F1 ??? X) (F1 ??? Y);
+ FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2
+}.
+
+definition Fm :
+ ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.
+ Fo ?? F → Fo ?? F → setoid2.
+intros (C1 C2 F X Y); constructor 1; [apply (Fm_c C1 C2 F X Y)]
+constructor 1; [apply (λf,g.Fm2 ????? f =_2 Fm2 ????? g);]
+[ intro; apply refl2;
+| intros 3; apply sym2; assumption;
+| intros 5; apply (trans2 ?? ??? x1 x2);]
+qed.
+
+definition F_id :
+ ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o.Fm ?? F o o.
+intros; constructor 1;
+ [ apply (id2 C2 (F2 ??? o));
+ | apply (id2 C1 (F1 ??? o));
+ | cases o; cases H; simplify; apply (respects_id2 ?? F);]
+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 ??? (Fm2 ????? f) (Fm2 ????? g));
+ | apply (comp2 C1 ??? (Fm1 ????? f) (Fm1 ????? g));
+ | apply hide; cases o1 in f; cases o2 in g; cases o3; clear o1 o2 o3;
+ cases H; cases H1; cases H2; intros 2; cases c; cases c1; clear c c1;
+ simplify; apply (.= (respects_comp2:?)); apply (e1‡e);]
+| intros 6; change with
+ ((Fm2 C1 C2 F o2 o3 b∘Fm2 C1 C2 F o1 o2 a) =
+ (Fm2 C1 C2 F o2 o3 b'∘Fm2 C1 C2 F o1 o2 a'));
+ change in e1 with (Fm2 ?? F ?? b = Fm2 ?? F ?? b');
+ change in e with (Fm2 ?? F ?? a = Fm2 ?? F ?? a');
+ apply (e‡e1);]
+qed.
+
+
+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; apply (comp_assoc2 C2 ???? (Fm2 ????? a12) (Fm2 ????? a23) (Fm2 ????? a34));
+| intros; apply (id_neutral_right2 C2 ?? (Fm2 ????? a));
+| intros; apply (id_neutral_left2 C2 ?? (Fm2 ????? a));]
+qed.
-o-basic_pairs.ma o-algebra.ma
+o-basic_pairs.ma notation.ma o-algebra.ma
basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
-o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
o-saturations.ma o-algebra.ma
saturations.ma relations.ma
+o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
basic_pairs.ma notation.ma relations.ma
-o-algebra.ma categories.ma
-o-formal_topologies.ma o-basic_topologies.ma
formal_topologies.ma basic_topologies.ma
+o-algebra.ma categories.ma
categories.ma cprop_connectives.ma
+o-formal_topologies.ma o-basic_topologies.ma
saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
-basic_topologies.ma relations.ma saturations.ma
subsets.ma categories.ma
+basic_topologies.ma relations.ma saturations.ma
concrete_spaces.ma basic_pairs.ma
+r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma
relations.ma subsets.ma
concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma
o-basic_topologies.ma o-algebra.ma o-saturations.ma
+notation.ma
basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
-notation.ma
+apply_functor.ma categories.ma
cprop_connectives.ma logic/connectives.ma
relations_to_o-algebra.ma o-algebra.ma relations.ma
-o-basic_pairs_to_o-basic_topologies.ma o-basic_pairs.ma o-basic_topologies.ma
+o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
logic/connectives.ma
| 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)).
-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.
-
-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)).
- REW ?? F X Y (map_arrows2 ?? F ?? g) = f)));
- | apply sigma_equivalence_relation2;]
-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);]
-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)))]
- cases o1; cases x; cases H;
-
-(* scrivo gli statement qua cosi' verra' un conflitto :-)
-
-1. definire il funtore OR
-2. dimostrare che ORel e' faithful
-
-3. Definire la funzione
- Apply:
- \forall 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
- | ....
- ]
-
- 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
- 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 ]
-
-5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
- quando applicato a rOBP.
- Nota: puo' darsi che faccia storie ad accettare lo statement.
- Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
- e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
- una "proiezione" da rOBP a OBP.
-
-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).
-
-8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
- esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
- faithful e full (banale: tutta conversione).
-
-9. Per composizione si ha un funtore full and faithful da BP a BTop.
-
-10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
- (http://planetmath.org/encyclopedia/DenseFunctor.html):
-
- BP_to_OBP
- OBP_to_OBTop quando applicato alle rOBP
- OBTop_to_BTop quando applicato alle rOBTop
-
- Concludere per composizione che anche il funtore da BP a BTop e'
- isomorphism-dense.
-
-====== Da qui in avanti non e' "necessario" nulla:
-
-== altre cose mancanti
-
-11. Dimostrare che le r* e le * orrizzontali
- sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
- due funtori ottengo l'identita'
-
-12. La definizione di r* fa schifo: in pratica dici solo come ottieni
- qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
- e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
- atomic. Dimostrarlo per tutte le r*.
-
-== categorish/future works
-
-13. definire astrattamente la FG-completion e usare quella per
- ottenere le BP da Rel e le OBP da OA.
-
-14. indebolire le OA, generalizzare le costruzioni, etc. come detto
- con Giovanni
-
-*)
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_pairs_to_o-basic_pairs.ma".
+include "apply_functor.ma".
+
+definition rOBP ≝ Apply ?? BP_to_OBP.
+
+include "o-basic_pairs_to_o-basic_topologies.ma".
+
+lemma rOR_full :
+ ∀rS,rT:rOBP.∀f:arrows2 ? (OR (F2 ??? rS)) (OR (F2 ??? rT)).
+ exT22 ? (λg:arrows2 OBP (F1 ??? rS) (F1 ??? rT).
+ map_arrows2 ? ? OR rS rT g = f).
+ ∀S,T.∀f. exT22 ? (λg. map_arrows2 ? ? OR S T g = f).
+arrows2 OBP S T
+unary_morphism1_setoid1 (OR S) (OR T)
+
+(* Todo: rename BTop → OBTop *)
+
+(* scrivo gli statement qua cosi' verra' un conflitto :-)
+
+1. definire il funtore OR
+2. dimostrare che ORel e' faithful
+
+3. Definire la funzione
+ Apply:
+ \forall 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
+ | ....
+ ]
+
+ 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
+ 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 ]
+
+5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
+ quando applicato a rOBP.
+ Nota: puo' darsi che faccia storie ad accettare lo statement.
+ Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
+ e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
+ una "proiezione" da rOBP a OBP.
+
+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).
+
+8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
+ esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
+ faithful e full (banale: tutta conversione).
+
+9. Per composizione si ha un funtore full and faithful da BP a BTop.
+
+10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
+ (http://planetmath.org/encyclopedia/DenseFunctor.html):
+
+ BP_to_OBP
+ OBP_to_OBTop quando applicato alle rOBP
+ OBTop_to_BTop quando applicato alle rOBTop
+
+ Concludere per composizione che anche il funtore da BP a BTop e'
+ isomorphism-dense.
+
+====== Da qui in avanti non e' "necessario" nulla:
+
+== altre cose mancanti
+
+11. Dimostrare che le r* e le * orrizzontali
+ sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
+ due funtori ottengo l'identita'
+
+12. La definizione di r* fa schifo: in pratica dici solo come ottieni
+ qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
+ e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
+ atomic. Dimostrarlo per tutte le r*.
+
+== categorish/future works
+
+13. definire astrattamente la FG-completion e usare quella per
+ ottenere le BP da Rel e le OBP da OA.
+
+14. indebolire le OA, generalizzare le costruzioni, etc. come detto
+ con Giovanni
+
+*)
+
projects / helm.git / commitdiff