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:

  _ (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'))

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.

    universal : βˆ€ x β†’ Universal-morphism x (Ο€αΆ  E)
    universal x .bot = record { y = x , system x ; map = }
    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.

    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