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 $\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 $t_1$ and $t_2$, then there is a unique isomorphism $t_1 \cong t_2$. We first establish the isomorphism: Since $t_1$ (resp. $t_2$) is terminal, there is a unique map $!_1 : t_1 \to t_2$ (resp. $!_2 : t_2 \to t_1$). To show these maps are inverses, we must show that $!_1 \circ !_2$ is $\id{id}$; But these morphisms inhabit a contractible space, namely the space of maps into $t_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 $C$ 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                         âˆŽ