抽象的に行く前に具象圏をいくつか紹介する。昨日は一つの圏の話しかしてこなかったので、これは役に立つことだと思う。
集合と全域関数 (total function) の圏は太字で Sets と表記する。
Scala では、大雑把に言うとこれは Int => String というように型と関数によってエンコードできる。
だけど、プログラミング言語はボトム型 (Nothing)、例外、停止しない (non-terminating) コードなどを許容するので、このエンコーディングが正しいのかという哲学的な議論があるらしい。便宜上、本稿ではこの問題を無視して Sets をエンコードできるふりをする。
全ての有限集合とその間の全域関数を Setsfin という。今まで見てきた圏がこれだ。