Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* (f:(AB). Bij(A; B; f))  (A ~~ B)	[bij_iff_1_1_corr]
Thm* f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A; B; f; g))	[bij_imp_exists_inv]
Thm* B:(AType), Q:(x:AB(x)Type). Thm* (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))	[dep_ax_choice]
Thm* Q:(ABProp). (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))	[ax_choice]
Def Surj(A; B; f) == b:B. a:A. f(a) = b	[surject]
Def A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)	[one_one_corr]

In prior sections: core

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html