こないだの稲見さんのスライドに Either<A, Never> = A とありましたが、これは集合における A ∪ φ = A に対応してそうです。一方で Pair<A, Void> = A というのは、 A × {1点} = A に対応してそうです。 (edited)

3:06 AM

集合の圏において空集合が始対象、一点が終対象であるのに対応して、型の圏では Never が始対象、Void が終対象で、両者の間で直和・直積を保つ綺麗な対応（圏から圏への対応 = 関手）があるんだろうと思います。 (edited)

3:09 AM

上の関係は a || false == a, a && true == a ともよく似ているので、ブール代数を圏と見た場合にも何らかの対応があるんだろうと思います。