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

Terminal objects are limits🔗

A terminal object is equivalently defined as a limit of the empty diagram.

is-limit→is-terminal
  :  {T : Ob} {eps : Const T => ¡F}
   is-limit {C = C} ¡F T eps
   is-terminal C T
is-limit→is-terminal lim Y = contr (lim.universal  ())  ()))
                                    _  sym (lim.unique _ _ _ λ ()))
  where module lim = is-limit lim

is-terminal→is-limit :  {T : Ob} {F : Functor ⊥Cat C}  is-terminal C T  is-limit {C = C} F T ¡nt
is-terminal→is-limit {T} {F} term = to-is-limitp ml λ {} where
  open make-is-limit
  ml : make-is-limit F T
  ml .ψ ()
  ml .commutes ()
  ml .universal _ _ = term _ .centre
  ml .factors {}
  ml .unique _ _ _ _ = sym (term _ .paths _)

Limit→Terminal : Limit {C = C} ¡F  Terminal C
Limit→Terminal lim .top = Limit.apex lim
Limit→Terminal lim .has⊤ = is-limit→is-terminal (Limit.has-limit lim)

Terminal→Limit :  {F : Functor ⊥Cat C}  Terminal C  Limit {C = C} F
Terminal→Limit term = to-limit (is-terminal→is-limit (term .has⊤))