|*: 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;