終対象 - pogi-log

終対象

終対象(final object, terminal object)、空積(empty product)

圏の中の任意の対象からただ一つの射がある対象を終対象と呼ぶ。

終対象は$ \mathbf{t}, \mathbf{1} で表されることが多いらしい。

$ C \to \mathbf{1}

証明については結城先生のやつを参照

対応するもの

(論理) true

(圏論) n-truncation: (-2)-truncated object

(型理論) unit type

(ホモトピー型理論) h-level 0型

HoTTでの対応

(homotopy level) h-level 0

(ホモトピー論) contractible space

(高次圏論) (-2)-groupoid

(高次トポス) -

(ホモトピー型理論) true

(ホモトピー型理論) unit type

(ホモトピー型理論) contractible type

確認用

Q. 終対象