(* ----------------------------------- *) ⊢
unary_morphism A B ≡ carr T.
+(*
ndefinition TYPE : setoid1.
@ setoid; @;
interpretation "new I" 'I a = (nI ? a).
ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
-(*
+
nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
#A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
nqed.
##[ @(f e);
*)
+(*
ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
#A; #a; #i; @ (image … i); #x; #y; #H; @;
##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
D*)
-*)
+*)*)
\ No newline at end of file