>>15
これSはreducedよね
π:S(X×Y)→SX∨S(X∧Y)∨SY
は普通のだと思うけど逆がよく分からん
i:SX,SY→S(X×Y)
はいいけど
S(X∧Y)→S(X×Y)
はどう定義するの?