始対象 - pogi-log

始対象

始対象(initial object)

$ \mathbf{0}

対象、射が集合である圏、小さい圏の圏$ \mathbf{Cat} は始対象が空圏$ \mathbf{0}

圏$ C のある対象を$ e ∈ \mathrm{Ob}(C) とする。

$ e が始対象$ \implies ∀X ∈ \mathrm{Ob}(C), ∃! f : e → X

各分野の対応

(論理) false

(集合) 空集合$ \emptyset

(圏論) 始対象

(型理論) 空型

確認用

Q. 始対象