open import Cat.Instances.Shape.Terminal
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Terminal where

module _ {o h} (C : Precategory o h) where
open Cat.Reasoning C


# 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
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β»ΒΉ)

module _ {o h} {C : Precategory o h} where
open Cat.Reasoning C
private unquoteDecl eqv = declare-record-iso eqv (quote Terminal)

instance
Extensional-Terminal
: β {βr}
β β¦ sa : Extensional Ob βr β¦
β Extensional (Terminal C) βr
Extensional-Terminal β¦ sa β¦ =
embeddingβextensional
(IsoβEmbedding eqv βemb (fst , Subset-proj-embedding (Ξ» _ β hlevel 1)))
sa