From 8844ee999e40d69795aa73fbeb198997a46fcf04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2009 11:21:07 +0000 Subject: [PATCH] ... --- .../overlap/basic_pairs_to_o-basic_pairs.ma | 18 ++++++++++++++++++ .../formal_topology/overlap/categories.ma | 5 ++--- .../overlap/relations_to_o-algebra.ma | 4 +--- 3 files changed, 21 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma index 7fc6a07f4..2dd4147ae 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma @@ -38,3 +38,21 @@ definition o_relation_pair_of_relation_pair: apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r))); apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] qed. + +(* +definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 cic:/matita/formal_topology/basic_pairs/BP.con) BP). + constructor 1; + [ apply o_basic_pair_of_basic_pair; + | intros; constructor 1; + [ apply (o_relation_pair_of_relation_pair S T); + | intros; split; unfold o_relation_pair_of_relation_pair; simplify; + unfold o_basic_pair_of_basic_pair; simplify; ] + | simplify; intros; whd; split; unfold o_relation_pair_of_relation_pair; simplify; + unfold o_basic_pair_of_basic_pair; +simplify in ⊢ (? ? ? (? % ? ?) ?); +simplify in ⊢ (? ? ? (? ? % ?) ?); +simplify in ⊢ (? ? ? ? (? % ? ?)); +simplify in ⊢ (? ? ? ? (? ? % ?)); + | simplify; intros; whd; split;unfold o_relation_pair_of_relation_pair; simplify; + unfold o_basic_pair_of_basic_pair;simplify; +*) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 7ac1b0b3d..af58968fc 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -302,9 +302,8 @@ record functor2 (C1: category2) (C2: category2) : Type3 ≝ map_arrows2: ∀S,T. unary_morphism2 (arrows2 ? S T) (arrows2 ? (map_objs2 S) (map_objs2 T)); respects_id2: ∀o:C1. map_arrows2 ?? (id2 ? o) = id2 ? (map_objs2 o); respects_comp2: - ∀o1,o2,o3,o4.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.∀f3:arrows2 ? o3 o4. - map_arrows2 ?? (f3 ∘ f2 ∘ f1) = - map_arrows2 ?? f3 ∘ map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}. + ∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3. + map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}. definition functor2_setoid: category2 → category2 → setoid3. intros (C1 C2); diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma index 7f2710640..2368affe0 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma @@ -168,9 +168,7 @@ definition SUBSETS': carr3 (arrows3 CAT2 (category2_of_category1 REL) OA). [ apply (orelation_of_relation S T); | intros; apply (orelation_of_relation_preserves_equality S T a a' e); ] | apply orelation_of_relation_preserves_identity; - | simplify; intros; - apply (.= (orelation_of_relation_preserves_composition o1 o2 o4 f1 (f3∘f2))); - apply (#‡(orelation_of_relation_preserves_composition o2 o3 o4 f2 f3)); ] + | apply orelation_of_relation_preserves_composition; ] qed. theorem SUBSETS_faithful: -- 2.39.2