S,T:Type. (n:. n ~ S) & (n:. n ~ T) (n:. n ~ (ST))

1	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))

About: