module Cat.Displayed.Total.Free {o β o' β'} {B : Precategory o β} (E : Displayed B o' β') where
Free objects in total categoriesπ
When the total category of a displayed category is being regarded as a category of structured , a natural question to consider is whether any object can be equipped with a free structure β in the sense of having a left adjoint to the projection functor
The displayed formulation admits a particularly nice phrasing of the condition for βhaving free objectsβ. To wit: a system of free objects for a displayed category is a section of the displayed object space β a function assigning objects to objects β having the property that these are βinitialβ among displayed maps:
module _ (system : β x β E.Ob[ x ]) (is-free : β {x y} (f : B.Hom x y) (y' : E.Ob[ y ]) β is-contr (E.Hom[ f ] (system x) y')) where
For any base morphism and displayed object there must be a contractible space of morphisms over The elegance of this definition speaks to the strength of the displayed framework for considering structured categories: It is a much shorter, and much more ergonomic, rephrasing of the condition that all comma categories have initial objects.
private universal : β x β Universal-morphism x (ΟαΆ E) universal x .bot = record { y = x , system x ; map = B.id } universal x .hasβ₯ m' = contr the-map unique where the-map : (x β ΟαΆ E) .Precategory.Hom (universal x .bot) m' the-map .Ξ± = tt the-map .Ξ² = total-hom (m' .map) (is-free (m' .map) (y m' .snd) .centre) the-map .sq = refl unique : β x β the-map β‘ x unique h = βHom-path _ _ refl $ total-hom-path E (B.intror refl Β·Β· h .sq Β·Β· B.elimr refl) (is-propβpathp (Ξ» i β is-contrβis-prop (is-free _ _)) _ _)
Since a system of free objects gives a system of universal morphisms, we have a left adjoint to the projection functor.
Free : Functor B (β« E) Free = universal-mapsβL (ΟαΆ E) universal Freeβ£ΟαΆ : Free β£ ΟαΆ E Freeβ£ΟαΆ = universal-mapsβLβ£R (ΟαΆ E) universal
Even though the Free
functor is produced by general
abstract nonsense, it admits an elementary description, which agrees
with the one above definitionally on objects, and differs on morphisms
by an extra identity map on the left.
private Free' : Functor B (β« E) Free' .Fβ o = o , system o Free' .Fβ h = total-hom h (is-free _ _ .centre) Free' .F-id = total-hom-path E refl (is-free _ _ .paths _) Free' .F-β f g = total-hom-path E refl (is-free _ _ .paths _) Freeβ‘Free' : Free β‘ Free' Freeβ‘Free' = Functor-path (Ξ» _ β refl) Ξ» f β total-hom-path E (B.idl _) Ξ» i β is-free (B.idl f i) (system _) .centre