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), g:(BA). InvFuns(A; B; f; g)  Bij(A; B; f)	[fun_with_inv_is_bij]
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]
Thm* f:(AB), g:(BA). SqStable(InvFuns(A; B; f; g))	[sq_stable__inv_funs]
Thm* f:(AB). f o Id = f	[comp_id_r]
Thm* f:(AB). Id o f = f	[comp_id_l]
Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f  AD	[comp_assoc]
Thm* f:(AB). (x.f(x)) = f	[eta_conv]
Def Surj(A; B; f) == b:B. a:A. f(a) = b	[surject]
Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2	[inject]

In prior sections: core

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