module Cat.Diagram.Terminal {o h} (C : Precategory o h) 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 β