Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
identity
Def
Id(
x
) ==
x
Thm*
A
:Type. Id
A
A
inject
Def
Inj(
A
;
B
;
f
) ==
a1
,
a2
:
A
.
f
(
a1
) =
f
(
a2
)
B
a1
=
a2
Thm*
A
,
B
:Type,
f
:(
A
B
). Inj(
A
;
B
;
f
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type. Id 
A
Aa1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(AB). Inj(A; B; f) PropA:Type. Id AAa1,a2:A. f(a1) = f(a2) B a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Prop
