🔍

Equations Inline Footnotes

open import Cat.Displayed.Instances.Lifting
open import Cat.Displayed.Isofibration
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Displayed.Functor
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Functor.Reasoning
import Cat.Reasoning
import Cat.Morphism

open Cat.Displayed.Morphism using (module _≅[_]_)
open Cat.Morphism._≅_
open _≅[_]_
open ∫Hom

module Cat.Displayed.Isofibration.Free where

Displayed categories from functors🔗

module _
  {ob ℓb oe ℓe}
  {B : Precategory ob ℓb}
  {E : Precategory oe ℓe}
  (P : Functor E B)
  where
  private
    module P = Cat.Functor.Reasoning P
    module E = Precategory E
    open Cat.Reasoning B

  open Displayed
  open Functor

This page addresses the problem of comparing notions in the theory of displayed categories, as we have formalised it, with those in the traditional study of relative category theory, which are stated in terms of a projection functor $P:\mathcal{E}\to \mathcal{B}\text{.}$ Essentially, we want to replace $\mathcal{E}$ with the total category of some displayed category $P_{\bullet }\mathcal{B}\text{,}$ so as to recover $P$ (up to equivalence) as the projection functor ${\pi }^f:\int P_{\bullet }\to \mathcal{B}\text{.}$

Fixing a functor $P:\mathcal{E}\to \mathcal{B}\text{,}$ we define the type of objects over $x:\mathcal{B}$ to consist of pairs $(x^{\prime },p)$ where $x^{\prime }:\mathcal{E}$ and $p:P(x^{\prime })\cong x$ — in other words, the objects over $x$ are not the type-theoretic fibre of $P$ over $x\text{,}$ but instead the category-theoretic essential fibre of $P$ over $x\text{.}$

  Free-isofibration : Displayed B (ℓb ⊔ oe) (ℓb ⊔ ℓe)
  Free-isofibration .Ob[_] x = Essential-fibre P x

To understand the types of maps in $P_{\bullet }\text{,}$ we will diagramatically denote a pair $(x^{\prime },p)x$ as a “leg”

A morphism $g:(x^{\prime },p){\to }_f(y^{\prime },q)$ lying over $f:x\to y$ is a map $\mathcal{E}(x^{\prime },y^{\prime })\text{,}$ which, “over” the Isomorphisms $p$ and $q\text{,}$ gets sent by $P$ to $f\text{.}$ Pictorially, we understand the type of $g$ as that of dashed arrows in the diagram below, where the “leg” $(x^{\prime },p)$ on the left (resp. $(y^{\prime },q)$ on the right) is drawn with $p$ towards the screen.

  Free-isofibration .Hom[_] f (x' , p) (y' , q) =
    Σ[ g ∈ E.Hom x' y' ] q .to ∘ P.₁ g ≡ f ∘ p .to

  Free-isofibration .Hom[_]-set f a b = hlevel 

  Free-isofibration .id' = record where
    fst = E.id
    snd = P.elimr refl ∙ introl refl

  Free-isofibration ._∘'_ (f , φ) (g , ψ) = record where
    fst = f E.∘ g
    snd = P.popl φ ∙ extendr ψ

  Free-isofibration .hom[_] p (f , α) = record
    { fst = f
    ; snd = α ∙ car p
    }
  Free-isofibration .coh[_] _ _   = Σ-prop-pathp! refl
  Free-isofibration .idr'   _     = Σ-prop-pathp! (E.idr _)
  Free-isofibration .idl'   _     = Σ-prop-pathp! (E.idl _)
  Free-isofibration .assoc' _ _ _ = Σ-prop-pathp! (E.assoc _ _ _)

module _
  {ob ℓb oe ℓe}
  {B : Precategory ob ℓb}
  {E : Precategory oe ℓe}
  (P : Functor E B)
  where
  private
    P∙ = Free-isofibration P

    module Iso[P] = Cat.Displayed.Morphism P∙
    module P = Cat.Functor.Reasoning P
    module B = Cat.Reasoning B
    module E = Cat.Reasoning E


  open Displayed-functor
  open Isofibration
  open Functor
  open Lifting

As an isofibration🔗

The construction of a displayed category from a functor results in an isofibration, and indeed this is the isofibration over $\mathcal{B}$ freely generated by $P\text{,}$ in a suitable bicategorical sense.

  Free-isofibration-iso
    : ∀ {a b x y}
    → {u : a B.≅ b} {φ : P.₀ x B.≅ a} {ψ : P.₀ y B.≅ b} (θ : x E.≅ y)
    → ψ .to B.∘ P.₁ (θ .to) ≡ u .to B.∘ φ .to
    → (x , φ) Iso[P].≅[ u ] (y , ψ)

  Free-isofibration-iso {u = u} {φ} {ψ} θ p =
    Iso[P].make-iso[ u ]
      (θ .to   , p)
      (θ .from , q)
      (Σ-prop-pathp! (θ .invl))
      (Σ-prop-pathp! (θ .invr))
    where abstract
      q : φ .to B.∘ P.₁ (θ .from) ≡ u .from B.∘ ψ .to
      q = flip Equiv.from refl $
        φ .to B.∘ P.₁ (θ .from) ≡ u .from B.∘ ψ .to     ≃⟨ B.post-invl (B.iso→invertible u) ⟩≃
        u .to B.∘ φ .to B.∘ P.₁ (θ .from) ≡ ψ .to       ≃⟨ ∙-pre-equiv (B.extendl p) ⟩≃
        ψ .to B.∘ P.₁ (θ .to) B.∘ P.₁ (θ .from) ≡ ψ .to ≃⟨ ∙-pre-equiv (B.intror (P.annihilate (θ .invl))) ⟩≃
        ψ .to ≡ ψ .to                                   ≃∎

With this in hand, showing that $P_{\bullet }$ is an isofibration is extremely straightforward. Supposing we have an iso $\psi :a\cong b\text{,}$ and drawing the object $(x,\phi )a$ we want to lift as a “leg”, we note that the lifting problem we have to solve involves a sequence of maps

whence it is immediate that the lifting we desire is $(x,\psi \circ \phi )\text{.}$

  Free-isofibration-is-isofibration : Isofibration P∙
  Free-isofibration-is-isofibration = record where
    _^*_ ψ (x , φ) = x , ψ B.∘Iso φ
    ^*-lifts ψ (x , φ) = Free-isofibration-iso
      E.id-iso
      (P.elimr refl)

The total category🔗

There is an evident lifting of $P_{\bullet }$ against $P\text{,}$ which sends an object $x:\mathcal{B}$ to the pair $(x,\mathrm{id}):P_x\text{.}$

  Free-isofibration-lifting : Lifting P∙ P
  Free-isofibration-lifting .F₀'  x   = x , B.id-iso
  Free-isofibration-lifting .F₁'  f   = f , B.id-comm-sym
  Free-isofibration-lifting .F-id'    = Σ-prop-pathp! refl
  Free-isofibration-lifting .F-∘' f g = Σ-prop-pathp! refl

  private
    E→∫ : Functor E (∫ P∙)
    E→∫ = Lifting→Functor _ Free-isofibration-lifting

  Free-isofibration-lifting-split-eso : is-split-eso E→∫
  Free-isofibration-lifting-is-ff     : is-fully-faithful E→∫

  Free-isofibration-lifting-split-eso (b , x , φ) = record where
    fst = x
    snd = iso[]→total-iso _ {x≅y = φ} $
      Free-isofibration-iso E.id-iso $ B.cdr P.F-id

  Free-isofibration-lifting-is-ff = is-iso→is-equiv λ where
    .is-iso.from h → h .snd .fst
    .is-iso.rinv h → ∫Hom-path _
      (B.introl refl ∙∙ h .snd .snd ∙∙ B.elimr refl)
      (Σ-prop-pathp! refl)
    .is-iso.linv h → refl

Finally, as desired, precomposition with this equivalence takes the projection functor ${\pi }^f$ to $P\text{.}$¹

  Free-isofibration-recovers : πᶠ P∙ F∘ E→∫ ≅ⁿ P
  Free-isofibration-recovers = Lifting-nat-iso _ _ ni⁻¹

  _ = sym (Lifting-is-lifting _ _)

Freeness as an isofibration🔗

To show that $P_{\bullet }$ is freely generated as an isofibration over $\mathcal{B}$ by $P\text{,}$ we show that any lifting of some other isofibration $\mathcal{H}\mathcal{B}$ against $P$ can be re-expressed as a vertical functor $P_{\bullet }\to H\text{.}$

  Free-isofibration-factor
    : ∀ {oh ℓh} {H : Displayed B oh ℓh}
    → Isofibration H → Lifting H P
    → Vertical-functor P∙ H
  Free-isofibration-factor {H = H} H-isofib F = F† where

    open Cat.Displayed.Reasoning H
    module H = Isofibration H-isofib
    module F = Lifting F renaming (F₀' to ₀' ; F₁' to ₁')

The gist of the construction is presented below. Starting with an object $(x,\phi ):P_a\text{,}$ we obtain an $F(x):{\mathcal{H}}_x\text{,}$ which we can transport to our desired ${\phi }^{\ast }F(x):{\mathcal{H}}_a$ since $\mathcal{H}$ is an isofibration.

    F† : Vertical-functor P∙ H
    F† .F₀' (x , φ) = φ H.^* F.₀' x
    F† .F₁' {a' = x , φ} {b' = y , ψ} (h , p) =
      hom[ B.pulll p ∙ B.cancelr (φ .invl) ] (H.π* ∘' F.₁' h ∘' H.ι!)

    F† .F-id' {x' = x , φ} = begin[]
      hom[] (H.π* ∘' F.₁' E.id ∘' H.ι!) ≡[]⟨ unwrap _ ⟩≡[]
      H.π* ∘' F.₁' E.id ∘' H.ι!         ≡[]⟨ refl⟩∘'⟨ eliml[] _ F.F-id' ⟩≡[]
      H.π* ∘' H.ι!                      ≡[]⟨ H.^*-lifts _ _ .invl' ⟩≡[]
      id'                               ∎[]

    F† .F-∘' {a' = x , φ} {b' = y , ψ} {c' = z , θ} {f' = f , p} {g' = g , q} =
      let
        open _≅[_]_ (H.^*-lifts φ (F.₀' x)) renaming (from' to φ^*→; to' to φ^*←)
        open _≅[_]_ (H.^*-lifts ψ (F.₀' y)) renaming (from' to ψ^*→; to' to ψ^*←)
        open _≅[_]_ (H.^*-lifts θ (F.₀' z)) renaming (from' to θ^*→; to' to θ^*←)
      in begin[]
        hom[] (θ^*← ∘' F.₁' (f E.∘ g) ∘' φ^*→)                           ≡[]⟨ unwrap _ ⟩≡[]
        θ^*← ∘' F.₁' (f E.∘ g) ∘' φ^*→                                   ≡[]⟨ refl⟩∘'⟨ (pushl[] _ (F.F-∘' f g)) ⟩≡[]
        θ^*← ∘' F.₁' f ∘' F.₁' g ∘' H.ι!                                 ≡[]⟨ refl⟩∘'⟨ refl⟩∘'⟨ (introl[] _ (H.^*-lifts _ _ .invr')) ⟩≡[]
        θ^*← ∘' F.₁' f ∘' (ψ^*→ ∘' ψ^*←) ∘' F.₁' g ∘' H.ι!               ≡[]⟨ refl⟩∘'⟨ refl⟩∘'⟨ pullr[] _ (wrap _) ⟩≡[]
        θ^*← ∘' F.₁' f ∘' ψ^*→ ∘' hom[] (ψ^*← ∘' F.₁' g ∘' φ^*→)         ≡[]⟨ pushr[] _ (assoc' _ _ _) ∙[] wrapl _ ⟩≡[]
        hom[] (θ^*← ∘' F.₁' f ∘' ψ^*→) ∘' hom[] (ψ^*← ∘' F.₁' g ∘' φ^*→) ∎[]