S,T:Type.
(
n:
, f:(n
S), g:(Sn). g o f = Id & f o g = Id)
& (n:, f:(nT), g:(Tn). g o f = Id & f o g = Id)
(n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id) S,T:Type.
(n:, f:(nS), g:(Sn). InvFuns(n; S; f; g))
& (n:, f:(nT), g:(Tn). InvFuns(n; T; f; g))
(n:, f:(nST), g:((ST)n). InvFuns(n; ST; f; g))| 1 | S,T:Type.
(n:, f:(nS), g:(Sn). g o f = Id & f o g = Id)
& (n:, f:(nT), g:(Tn). g o f = Id & f o g = Id)
(n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id) |
About:
 |  |  |  |  |  |  |  |