X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations_to_o-algebra.ma;h=842219280ba10fcfe19eba1af70f08b4f8944197;hb=be0ca791abbf1084b7218f2d17ab48462fbb3049;hp=af3015eb368737d5f62f3ce5c8689399edfc9e07;hpb=3e094922bf3fec6975fdbe6feceb509eaafe0563;p=helm.git

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 af3015eb3..842219280 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
@@ -182,8 +182,25 @@ theorem POW_faithful:
   |*: cases Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;]
 qed.
 
+
+lemma currify: ∀A,B,C. binary_morphism1 A B C → A → unary_morphism1 B C.
+intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
+qed.
+
+(*
+alias symbol "singl" = "singleton".
+alias symbol "eq" = "setoid eq".
+lemma in_singleton_to_eq : ∀A:setoid.∀y,x:A.y ∈ {(x)} → (eq1 A) y x.
+intros; apply sym1; apply f;
+qed.  
+
+lemma eq_to_in_singleton : ∀A:setoid.∀y,x:A.eq1 A y x → y ∈ {(x)}.
+intros; apply (e^-1);
+qed.
+*)
+
 interpretation "lifting singl" 'singl x = 
- (fun11 _ (objs2 (POW _))  (singleton _) x).
+ (fun11 ? (objs2 (POW ?))  (singleton ?) x).
 
 theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
  intros; exists;