open import Cat.Univalent
open import Cat.Prelude

module Cat.Diagram.Terminal {o h} (C : Precategory o h) where

Terminal objectsπŸ”—

An object ⊀\top of a category C\mathcal{C} is said to be terminal if it admits a unique map from any other object:

is-terminal : Ob β†’ Type _
is-terminal ob = βˆ€ x β†’ is-contr (Hom x ob)

record Terminal : Type (o βŠ” h) where
  field
    top : Ob
    has⊀ : is-terminal top

We refer to the centre of contraction as !. Since it inhabits a contractible type, it is unique.

  ! : βˆ€ {x} β†’ Hom x top
  ! = has⊀ _ .centre

  !-unique : βˆ€ {x} (h : Hom x top) β†’ ! ≑ h
  !-unique = has⊀ _ .paths

  !-uniqueβ‚‚ : βˆ€ {x} (f g : Hom x top) β†’ f ≑ g
  !-uniqueβ‚‚ = is-contrβ†’is-prop (has⊀ _)

open Terminal

UniquenessπŸ”—

If a category has two terminal objects t1t_1 and t2t_2, then there is a unique isomorphism t1β‰…t2t_1 \cong t_2. We first establish the isomorphism: Since t1t_1 (resp. t2t_2) is terminal, there is a unique map !1:t1β†’t2!_1 : t_1 \to t_2 (resp. !2:t2β†’t1!_2 : t_2 \to t_1). To show these maps are inverses, we must show that !1∘!2!_1 \circ !_2 is id\id{id}; But these morphisms inhabit a contractible space, namely the space of maps into t2t_2, so they are equal.

!-invertible : (t1 t2 : Terminal) β†’ is-invertible (! t1 {top t2})
!-invertible t1 t2 = make-invertible (! t2) (!-uniqueβ‚‚ t1 _ _) (!-uniqueβ‚‚ t2 _ _)

⊀-unique : (t1 t2 : Terminal) β†’ top t1 β‰… top t2
⊀-unique t1 t2 = invertibleβ†’iso (! t2) (!-invertible t2 t1)

Hence, if CC is additionally a category, it has a propositional space of terminal objects:

⊀-contractible : is-category C β†’ is-prop Terminal
⊀-contractible ccat x1 x2 i .top =
  isoβ†’path C ccat (⊀-unique x1 x2) i

⊀-contractible ccat x1 x2 i .has⊀ ob =
  is-prop→pathp
    (Ξ» i β†’ is-contr-is-prop {A = Hom _
      (isoβ†’path C ccat (⊀-unique x1 x2) i)})
    (x1 .has⊀ ob) (x2 .has⊀ ob) i

is-terminal-iso : βˆ€ {A B} β†’ A β‰… B β†’ is-terminal A β†’ is-terminal B
is-terminal-iso isom term x = contr (isom .to ∘ term x .centre) Ξ» h β†’
  isom .to ∘ term x .centre β‰‘βŸ¨ ap (isom .to ∘_) (term x .paths _) βŸ©β‰‘
  isom .to ∘ isom .from ∘ h β‰‘βŸ¨ cancell (isom .invl) βŸ©β‰‘
  h                         ∎