open import Cat.Instances.Functor
open import Cat.Diagram.Initial
open import Cat.Displayed.Total
open import Cat.Instances.Comma
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning as Cr

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:

private
module B = Cr B
module E = Displayed E
open Initial
open Functor
open βObj
open βHom

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