プログラミング言語や型理論の文脈で、空リストの型つけ〈タイピング〉が話題になることがあります。集合論と圏論で解釈してみると、結果が違ってきます。発想が違うので結果がズレるのは驚くことではありませんが、意外に思う人もいるかも知れません。内容…