X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations.ma;h=c4502f3d080b61874360cfb4e650bde1f3b99694;hb=49045bfd9b3038ce30a1911e2345f949ed38ec8a;hp=dc3c091bbfe49d75ba005997b44ef38b386db4d6;hpb=33fbecf99c187fb4fc84a68ee9f479da046e9df9;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index dc3c091bb..c4502f3d0 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -96,14 +96,12 @@ definition REL: category1.
           first [apply refl | assumption]]]
 qed.
 
-(*
 definition full_subset: ∀s:REL. Ω \sup s.
  apply (λs.{x | True});
  intros; simplify; split; intro; assumption.
 qed.
 
 coercion full_subset.
-*)
 
 definition setoid1_of_REL: REL → setoid ≝ λS. S.
 coercion setoid1_of_REL.
@@ -114,23 +112,27 @@ lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 →
 qed.
 coercion Type_OF_setoid1_of_REL.
 
-(*
-definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
- intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+ intros; simplify;
+ alias symbol "trans" = "trans1".
+ alias symbol "prop1" = "prop11".
+ apply (.= †e); apply refl1.
 qed.
 
 interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
+ (comprehension s (mk_unary_morphism1 __ p _)).
 
 definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
- apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
-  [ intros; simplify; apply (.= (H‡#)); apply refl1
-  | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
-     [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
-     | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (e‡#)); apply refl1
+  | intros; simplify; split; intros; simplify;
+     [ change with (∀x. x ♮a b → x ♮a' b'); intros;
+       apply (. (#‡e1)); whd in e; apply (if ?? (e ??)); assumption
+     | change with (∀x. x ♮a' b' → x ♮a b); intros;
+       apply (. (#‡e1\sup -1)); whd in e; apply (fi ?? (e ??));assumption]]
 qed.
-
+(*
 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
  intros (X S r); constructor 1;