1. A,B:Type, f:(AB), g:(BA). g o f = Id  (x:A. g(f(x)) = x)
  A,B:Type, f:(AB), g:(BA).
  g o f = Id & f o g = Id  (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

None

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