Definitions
fun
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
inv_funs
Def
InvFuns(
A
;
B
;
f
;
g
) ==
g
o
f
= Id &
f
o
g
= Id
Thm*
A
,
B
:Type,
f
:(
A
B
),
g
:(
B
A
). InvFuns(
A
;
B
;
f
;
g
)
Prop
sq_stable
Def
SqStable(
P
) ==
P
P
Thm*
A
:Prop. SqStable(
A
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
fun
1
Sections
StandardLIB
Doc
A,B:Type, f:(A
B), g:(BA). InvFuns(A; B; f; g) 
Prop
P 
PA:Prop. SqStable(A) PropA,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) PropP PA:Prop. SqStable(A) Prop
