Selected Objects

Introduction		Introductory Remarks
THM	eta_conv	f:(AB). (x.f(x)) = f
def	tlambda	(x:T. b(x))(x) == b(x)
def	identity	Id(x) == x
def	tidentity	Id == Id
def	compose	(f o g)(x) == f(g(x))
THM	comp_assoc	f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f  AD
THM	comp_id_l	f:(AB). Id o f = f
THM	comp_id_r	f:(AB). f o Id = f
def	inv_funs	InvFuns(A; B; f; g) == g o f = Id & f o g = Id
THM	sq_stable__inv_funs	f:(AB), g:(BA). SqStable(InvFuns(A; B; f; g))
def	one_one_corr	A ~~ B == f:(AB), g:(BA). InvFuns(A; B; f; g)
def	inject	Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2
def	surject	Surj(A; B; f) == b:B. a:A. f(a) = b
def	biject	Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)
THM	ax_choice	Q:(ABProp). (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))
THM	dep_ax_choice	B:(AType), Q:(x:AB(x)Type). (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))
THM	bij_imp_exists_inv	f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A; B; f; g))
THM	fun_with_inv_is_bij	f:(AB), g:(BA). InvFuns(A; B; f; g)  Bij(A; B; f)
THM	bij_iff_1_1_corr	(f:(AB). Bij(A; B; f))  (A ~~ B)

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html