From 8abe6fae9e3c76b7d94090e3373204890e0be11c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 01:39:36 +0000 Subject: [PATCH] An hint moved to the right place. --- .../matita/contribs/formal_topology/overlap/categories.ma | 6 ++++++ .../matita/contribs/formal_topology/overlap/relations.ma | 8 +------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 3a7614fca..3ee391507 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -372,6 +372,12 @@ definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1. qed. coercion Type1_OF_SET1. +definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*). + [ apply setoid1_of_SET; apply U + | intros; apply c;] +qed. +coercion Type_OF_setoid1_of_carr. + 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). diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index eb60386fe..ed8b83bcb 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -175,12 +175,6 @@ lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (e qed. *) -lemma hint: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*). - [ apply setoid1_of_SET; apply U - | intros; apply c;] -qed. -coercion hint. - (* the same as ⋄ for a basic pair *) definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V). intros; constructor 1; @@ -327,4 +321,4 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (S | cases x1; cases x2; clear x1 x2; exists; [apply w1] [ exists; [apply w] split; assumption; | assumption; ]]] -qed. (*sistemare anche l'hint da un'altra parte *) +qed. -- 2.39.2