From 2f57490a8df5e3e5c09b238f99e34067015a7df3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 3 Jan 2009 18:27:07 +0000 Subject: [PATCH] Niceness was just a temporary illusion :-( --- .../formal_topology/overlap/categories.ma | 5 +++++ .../overlap/o-basic_topologies.ma | 16 +++++++--------- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index f09e0ee6c..1452652fa 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -404,3 +404,8 @@ coercion Type1_OF_SET1. interpretation "SET dagger" 'prop1 h = (prop11_SET1 _ _ _ _ _ h). interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b). interpretation "SET1 eq" 'eq x y = (eq_rel1 _ (eq'' _) x y). + +lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T. + intros; apply t; +qed. +coercion unary_morphism1_of_arrows1_SET1. \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index 640a936ee..be985a43c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -135,11 +135,6 @@ definition continuous_relation_comp: | apply refl1]] qed. -lemma hintx: ∀S,T. (S ⇒ T) → unary_morphism1 S T. - intros; apply t; -qed. -coercion hintx. - definition BTop: category2. constructor 1; [ apply basic_topology @@ -160,13 +155,16 @@ definition BTop: category2. change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x))); alias symbol "trans" = "trans1". alias symbol "prop1" = "prop11". - apply (.= †(saturated o1 o2 a' (A o1 x) : ?)); - [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1); ] + alias symbol "invert" = "setoid1 symmetry". + lapply (.= †(saturated o1 o2 a' (A o1 x) : ?)); + [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip; + |apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1); ] change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x)); apply (.= (e1 (a'⎻* (A o1 x)))); alias symbol "invert" = "setoid1 symmetry". - apply (†((saturated ?? a' (A o1 x) : ?) ^ -1)); - apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1);] + lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1)); + [2: apply (b'⎻* ); |4: apply Hletin; | skip; + |apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1);]] | intros; simplify; change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1)); apply rule (#‡ASSOC1\sup -1); -- 2.39.2