IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one one corr fams if bij A1111 1. A : Type
2. A' : Type
3. AType
4. g : A'A 5. Bij(A'; A; g)
6. f : AA' 7. InvFuns(A';A;g;f)
8. y : A g(f(y)) = y
By:
BackThru: InvFuns(A';A;g;f)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html