Selected Objects
Introduction | Introductory Remarks |
THM | eta_conv |
f:(A B). ( 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:(A B), g:(B C), h:(C D). h o (g o f) = (h o g) o f A D |
THM | comp_id_l |
f:(A B). Id o f = f |
THM | comp_id_r |
f:(A B). 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:(A B), g:(B A). SqStable(InvFuns(A; B; f; g)) |
def | one_one_corr |
A ~~ B == f:(A B), g:(B A). 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:(A B Prop). ( x:A. y:B. Q(x,y))  ( f:(A B). x:A. Q(x,f(x))) |
THM | dep_ax_choice |
B:(A Type), Q:(x:A B(x) Type).
( x:A. y:B(x). Q(x,y))  ( f:(x:A B(x)). x:A. Q(x,f(x))) |
THM | bij_imp_exists_inv |
f:(A B). Bij(A; B; f)  ( g:(B A). InvFuns(A; B; f; g)) |
THM | fun_with_inv_is_bij |
f:(A B), g:(B A). InvFuns(A; B; f; g)  Bij(A; B; f) |
THM | bij_iff_1_1_corr |
( f:(A B). Bij(A; B; f))  (A ~~ B) |