module Cat.Diagram.Terminal where

Terminal objectsπŸ”—

An object of a category 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 and then there is a unique isomorphism We first establish the isomorphism: Since (resp. is terminal, there is a unique map (resp. To show these maps are inverses, we must show that is But these morphisms inhabit a contractible space, namely the space of maps into 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 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 =
    ccat .to-path (⊀-unique x1 x2) i

  ⊀-contractible ccat x1 x2 i .has⊀ ob =
    is-prop→pathp
      (Ξ» i β†’ is-contr-is-prop {A = Hom _
        (ccat .to-path (⊀-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                         ∎

In terms of right adjointsπŸ”—

We prove that the inclusion functor of an object of is right adjoint to the unique functor if and only if is terminal.

  module _ (x : Ob) (term : is-terminal x) where
    is-terminalβ†’inclusion-is-right-adjoint : !F ⊣ !Const {C = C} x
    is-terminal→inclusion-is-right-adjoint =
      hom-iso→adjoints (e _ .fst) (e _ .snd)
        Ξ» _ _ _ β†’ term _ .paths _
      where
        e : βˆ€ y β†’ ⊀ ≃ Hom y x
        e y = is-contr→≃ (hlevel 0) (term y)

  module _ (x : Ob) (adj : !F ⊣ !Const {C = C} x) where
    inclusion-is-right-adjoint→is-terminal : is-terminal x
    inclusion-is-right-adjoint→is-terminal y = Equiv→is-hlevel 0
      (Ξ£-contract (Ξ» _ β†’ hlevel 0) e⁻¹)
      (R-adjunct-is-equiv adj .is-eqv _)