From f1889c6a0850d2691190d34159d5eb9bb9c76f77 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 22 Dec 2008 18:07:42 +0000 Subject: [PATCH] Some clean up. --- .../contribs/formal_topology/overlap/o-algebra.ma | 7 +------ .../formal_topology/overlap/o-concrete_spaces.ma | 9 +-------- .../matita/library/datatypes/categories.ma | 15 ++++++++++++++- 3 files changed, 16 insertions(+), 15 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index 4c61f0fb4..0cb3fe117 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -26,11 +26,6 @@ constructor 1; [apply bool] constructor 1; try assumption; apply I] qed. -definition setoid_OF_SET: objs1 SET → setoid. - intros; apply o; qed. - -coercion setoid_OF_SET. - lemma IF_THEN_ELSE_p : ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y → (λm.match m with [ true ⇒ a | false ⇒ b ]) x = @@ -297,4 +292,4 @@ split; | apply ((comp_assoc1 ????? H* G* F* ));] | intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1; | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index 80ee4649f..5b08b5917 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -118,13 +118,6 @@ definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 coercion rp''. -definition prop_1_SET : - ∀A,B:SET.∀w:arrows1 SET A B.∀a,b:A.eq1 ? a b→eq1 ? (w a) (w b). -intros; apply (prop_1 A B w a b H); -qed. - -interpretation "SET dagger" 'prop1 h = (prop_1_SET _ _ _ _ _ h). - definition convergent_relation_space_composition: ∀o1,o2,o3: concrete_space. binary_morphism1 @@ -170,4 +163,4 @@ definition CSPA: category1. | intros; simplify; change with (id1 ? o2 ∘ a = a); apply (id_neutral_left1 : ?);] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma index ca49cbdd3..65bc8ac6b 100644 --- a/helm/software/matita/library/datatypes/categories.ma +++ b/helm/software/matita/library/datatypes/categories.ma @@ -236,4 +236,17 @@ definition SET: category1. | intros; simplify; whd; intros; simplify; apply refl; | intros; simplify; whd; intros; simplify; apply refl; ] -qed. \ No newline at end of file +qed. + +definition setoid_OF_SET: objs1 SET → setoid. + intros; apply o; qed. + +coercion setoid_OF_SET. + + +definition prop_1_SET : + ∀A,B:SET.∀w:arrows1 SET A B.∀a,b:A.eq1 ? a b→eq1 ? (w a) (w b). +intros; apply (prop_1 A B w a b H); +qed. + +interpretation "SET dagger" 'prop1 h = (prop_1_SET _ _ _ _ _ h). -- 2.39.2