module Cat.Displayed.Instances.Lifting where

Liftings🔗

A category E\mathcal{E} displayed over B\mathcal{B} contains the same data as a functor into B\mathcal{B}, just packaged in a way that makes it easier to talk about lifting properties. If we take this perspective, we can start considering diagrams of functors. In particular, we can consider lifts of functors F:JBF : \mathcal{J} \to \mathcal{B}, as in the following diagram:

If we unfold this in terms of displayed categories, such a lifting L:JEL : \mathcal{J} \to \mathcal{E} would give a J\mathcal{J}-shaped diagram in E\mathcal{E} lying over a corresponding diagram in B\mathcal{B}.

  record Lifting (F : Functor J B) : Type (o'  ℓ'  oj  ℓj) where
    no-eta-equality
    field
      F₀'   : (j : J.Ob)  Ob[ F .F₀ j ]
      F₁'   :  {i j}  (f : J.Hom i j)  Hom[ F .F₁ f ] (F₀' i) (F₀' j)

      F-id' :  {j}  F₁' (J.id {j}) ≡[ F .F-id ] id'
      F-∘'  :  {i j k} (f : J.Hom j k) (g : J.Hom i j)
             F₁' (f J.∘ g) ≡[ F .F-∘ f g ] F₁' f ∘' F₁' g

  open Lifting

Liftings of a functor F:JBF : \mathcal{J} \to \mathcal{B} yield functors from J\mathcal{J} to the total category of E\mathcal{E}.

  Lifting→Functor :  {F : Functor J B}  Lifting F  Functor J ( E)
  Lifting→Functor {F} F' .F₀ j = F .F₀ j , F' .F₀' j
  Lifting→Functor {F} F' .F₁ f = total-hom (F .F₁ f) (F' .F₁' f)
  Lifting→Functor {F} F' .F-id = total-hom-path E (F .F-id) (F' .F-id')
  Lifting→Functor {F} F' .F-∘ f g = total-hom-path E (F .F-∘ f g) (F' .F-∘' f g)

Furthermore, such liftings commute extremely strictly. Not only are the two functors equal, the action on objects and morphisms are definitionally equal! This highlights the utility of the theory of displayed categories; by reorganizing our data, we can talk about a higher level of strictness than usual.

  Lifting-is-lifting
    :  {F : Functor J B}  (F' : Lifting F)
     F  (πᶠ E F∘ Lifting→Functor F')
  Lifting-is-lifting F' = Functor-path  _  refl)  f  refl)

  Lifting-nat-iso
    :  {F : Functor J B}  (F' : Lifting F)
     F ≅ⁿ πᶠ E F∘ Lifting→Functor F'
  Lifting-nat-iso F' = to-natural-iso ni where
    open make-natural-iso

    ni : make-natural-iso _ _
    ni .eta _ = id
    ni .inv _ = id
    ni .eta∘inv _ = idl _
    ni .inv∘eta _ = idl _
    ni .natural _ _ _ = id-comm

Natural transformations between liftings🔗

As liftings are a reorganization of functors, it is reasonable to expect that we can express natural transformations between these. Fix functors F,G:JBF, G : \mathcal{J} \to \mathcal{B}, and let F,GF', G' be their liftings along π:EB\pi : \mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}. Furthermore, let α:FG\alpha : F \to G be a natural transformation. A natural transformation of liftings between FF' and GG' over α\alpha is given by a family of morphisms ηj\eta_{j} between F(j)F'(j) and G(j)G'(j).

  record _=[_]=>l_
    {F G : Functor J B}
    (F' : Lifting E F) (α : F => G) (G' : Lifting E G)
    : Type (ℓ'  oj  ℓj) where
    no-eta-equality

    field
      η' :  (j)  Hom[ α .η j ] (F' .F₀' j) (G' .F₀' j)

      is-natural' :  (i j : J.Ob) (f : J.Hom i j)
                   η' j ∘' F' .F₁' f ≡[ α .is-natural i j f ] G' .F₁' f  ∘' η' i

Diagramatically, the situation is as follows:

As expected natural transformations of liftings yield natural transformations between the associated functors.

  Nat-lift→Nat
    :  {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G}
     {α : F => G}  F' =[ α ]=>l G'  Lifting→Functor E F' => Lifting→Functor E G'
  Nat-lift→Nat {α = α} α' .η x .hom = α .η x
  Nat-lift→Nat {α = α} α' .η x .preserves = α' .η' x
  Nat-lift→Nat {α = α} α' .is-natural x y f =
    total-hom-path E (α .is-natural x y f) (α' .is-natural' x y f)

As liftings are definitional, any natural transformation FGF \to G is also a natural transformation πFπG\pi \circ F' \to \pi \circ G'; showing this requires repacking some data due to the lack of some η\eta-rules.

  Nat→Nat-lift
    :  {F G : Functor J B} (F' : Lifting E F) (G' : Lifting E G)
     F => G  πᶠ E F∘ Lifting→Functor E F' => πᶠ E F∘ Lifting→Functor E G'
  Nat→Nat-lift F' G' α .η          = α .η
  Nat→Nat-lift F' G' α .is-natural = α .is-natural

This allows us to characterize natural transformations of liftings: they are precisely the natural transformations that definitionally lie over their bases.

  Nat-lift-is-lifting
    :  {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G}
     {α : F => G}  (α' : F' =[ α ]=>l G')
     πᶠ E  Nat-lift→Nat α'  Nat→Nat-lift F' G' α
  Nat-lift-is-lifting α' = Nat-path  _  refl)

The identity natural transformation is easy to define, as is vertical composition.

  idntl :  {F : Functor J B} {F' : Lifting E F}  F' =[ idnt ]=>l F'
  idntl .η' j = id'
  idntl .is-natural' i j f = idl' _ ∙[] symP (idr' _)

  _∘ntl_
    :  {F G H : Functor J B} {F' : Lifting E F} {G' : Lifting E G} {H' : Lifting E H}
     {α : G => H} {β : F => G}
     G' =[ α ]=>l H'  F' =[ β ]=>l G'  F' =[ α ∘nt β ]=>l H'
  _∘ntl_ α' β' .η' j = α' .η' j ∘' β' .η' j
  _∘ntl_  {F' = F'} {G'} {H'} α' β' .is-natural' i j f' =
    (α' .η' j ∘' β' .η' j) ∘' F' .F₁' f' ≡[]⟨ pullr[] _ (β' .is-natural' i j f') ≡[]
    α' .η' j ∘' G' .F₁' f' ∘' β' .η' i   ≡[]⟨ extendl[] _ (α' .is-natural' i j f') ≡[]
    H' .F₁' f' ∘' α' .η' i ∘' β' .η' i   

The fibration of liftings🔗

The liftings of functors JB\mathcal{J} \to \mathcal{B} assemble into a displayed category over the functor category [J,B][\mathcal{J}, \mathcal{B}]. We shall denote this category EJ\mathcal{E}^{\mathcal{J}}, as it is the displayed analog of the fibration π:EJBJ\pi \circ - : \mathcal{E}^{\mathcal{J}} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}^{\mathcal{J}}, where π:EB\pi : \mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} is a fibration.

  Liftings : Displayed Cat[ J , B ] (o'  ℓ'  oj  ℓj) (ℓ'  oj  ℓj)
  Liftings .Displayed.Ob[_] = Lifting E
  Liftings .Displayed.Hom[_] α F' G' = F' =[ α ]=>l G'
  Liftings .Displayed.Hom[_]-set _ _ _ = Nat-lift-is-set
  Liftings .Displayed.id' = idntl
  Liftings .Displayed._∘'_ = _∘ntl_
  Liftings .Displayed.idr' _ = Nat-lift-pathp  _  idr' _)
  Liftings .Displayed.idl' _ = Nat-lift-pathp  _  idl' _)
  Liftings .Displayed.assoc' _ _ _ = Nat-lift-pathp  _  assoc' _ _ _)

If a natural transformation of liftings is pointwise cartesian, then it is cartesian.

  pointwise-cartesian→Liftings-cartesian
    :  {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G}
     {α : F => G} {α' : F' =[ α ]=>l G'}
     (∀ x  is-cartesian E (α .η x) (α' .η' x))
     is-cartesian Liftings α α'
  pointwise-cartesian→Liftings-cartesian {α = α} {α' = α'} pointwise = cart where
    module pointwise x = is-cartesian (pointwise x)

    cart : is-cartesian Liftings α α'
    cart .is-cartesian.universal β γ' .η' x =
      pointwise.universal x (β .η x) (γ' .η' x)
    cart .is-cartesian.universal β γ' .is-natural' x y f =
      pointwise.uniquep₂ _ _ _ _ _ _
        (pulll[] _ (pointwise.commutes _ _ _) ∙[] γ' .is-natural' _ _ _)
        (pulll[] _ (α' .is-natural' x y f)
        ∙[] pullr[] _ (pointwise.commutes _ _ _))
    cart .is-cartesian.commutes β γ' =
      Nat-lift-pathp  _  pointwise.commutes _ _ _)
    cart .is-cartesian.unique γ' p =
      Nat-lift-pathp  x  pointwise.unique _ _ λ i  p i .η' x)

When E\mathcal{E} is a fibration, then so is the displayed category of liftings.

  Liftings-fibration
    : (fib : Cartesian-fibration E)
     Cartesian-fibration Liftings
  Liftings-fibration fib .Cartesian-fibration.has-lift {F} {G} α G' = cart-lift where
    module F = Functor F
    module G = Functor G
    open Cartesian-fibration fib
    open Lifting
    open _=[_]=>l_

We begin by constructing the lifting over FF; we can do this by reindexing GG' pointwise.

    G'* : Lifting E F
    G'* .F₀' j = has-lift.x' (α .η j) (G' .F₀' j)
    G'* .F₁' f =
      has-lift.universal _ _ _
        (hom[ α .is-natural _ _ f ]⁻ (G' .F₁' f ∘' has-lift.lifting _ _))
The functoriality proofs are a bit gnarly, so we leave them in this <details> block.
    G'* .F-id' =
      symP $ has-lift.uniquep _ _ _ (sym (F .F-id)) (α .is-natural _ _ _) id' $
        has-lift.lifting _ _ ∘' id'          ≡[]⟨ idr' _ ≡[]
        has-lift.lifting _ _                 ≡[]⟨ symP (idl' _) ≡[]
        id' ∘' has-lift.lifting _ _          ≡[]⟨  i  G' .F-id' (~ i) ∘' has-lift.lifting (α .η _) (G' .F₀' _)) ≡[]
        G' .F₁' J.id ∘' has-lift.lifting _ _ 

    G'* .F-∘' f g =
      symP $ has-lift.uniquep _ _ _
        (sym (F .F-∘ f g)) (α .is-natural _ _ _ ) (G'* .F₁' f ∘' G'* .F₁' g) $
          has-lift.lifting _ _ ∘' G'* .F₁' f ∘' G'* .F₁' g        ≡[]⟨ pulll[] _ (has-lift.commutes _ _ _ _) ≡[]
          hom[] (G' .F₁' f ∘' has-lift.lifting _ _) ∘' G'* .F₁' g ≡[ ap (_∘ F.F₁ g) (α .is-natural _ _ _) ]⟨ to-pathp⁻ (whisker-l (sym (α .is-natural _ _ _))) ]
          (G' .F₁' f ∘' has-lift.lifting _ _) ∘' G'* .F₁' g       ≡[]⟨ pullr[] _ (has-lift.commutes _ _ _ _) ≡[]
          G' .F₁' f ∘' hom[] (G' .F₁' g ∘' has-lift.lifting _ _)  ≡[ ap (G.F₁ f ∘_) (α .is-natural _ _ _) ]⟨ to-pathp⁻ (whisker-r (sym (α .is-natural _ _ _))) ]
          G' .F₁' f ∘' (G' .F₁' g ∘' has-lift.lifting _ _)        ≡[]⟨ pulll[] _ (symP (G' .F-∘' f g)) ≡[]
          G' .F₁' (f J.∘ g) ∘' has-lift.lifting _ _               

As we have constructed the lift of GG via reindexing, we can use the existing cartesian lifts to build the lift of α\alpha. This also implies that our natural transformation is cartesian.

    α'* : G'* =[ α ]=>l G'
    α'* .η' x = has-lift.lifting (α .η x) (G' .F₀' x)
    α'* .is-natural' x y f = has-lift.commutesp (α .η y) (G' .F₀' y) _ _

    cart-lift : Cartesian-lift Liftings α G'
    cart-lift .Cartesian-lift.x' = G'*
    cart-lift .Cartesian-lift.lifting = α'*
    cart-lift .Cartesian-lift.cartesian =
      pointwise-cartesian→Liftings-cartesian
         x  has-lift.cartesian (α .η x) (G' .F₀' x))

Total category🔗

As noted earlier, the total category of EJ\mathcal{E}^{\mathcal{J}} is the functor category [J,E][\mathcal{J}, \int \mathcal{E}]. First, we shall need a heaping pile of repackaging lemmas.

  ∫Functor→Lifting         : (F : Functor J ( E))  Lifting E (πᶠ E F∘ F)
  Functor+Lifting→∫Functor : (F : Functor J B)  Lifting E F  Functor J ( E)

  ∫Nat→Nat :  {F G : Functor J ( E)}  F => G  πᶠ E F∘ F => πᶠ E F∘ G
  Nat+Nat-lift→∫Nat
    :  {F G : Functor J ( E)}
     (α : πᶠ E F∘ F => πᶠ E F∘ G)
     (α' : ∫Functor→Lifting F =[ α ]=>l ∫Functor→Lifting G)
     F => G

  ∫Nat→Nat-lift
    :  {F G : Functor J ( E)}  (α : F => G)
     ∫Functor→Lifting F =[ ∫Nat→Nat α ]=>l ∫Functor→Lifting G

Since none of these constructions have deeper mathematical content than their types, we omit the definitions from the page entirely.

Using these repackagings, we can define the promised functor from [J,E][\mathcal{J}, \int \mathcal{E}] into the total category of the fibration of liftings.

  Functors→Liftings : Functor Cat[ J ,  E ] ( Liftings)
  Functors→Liftings .F₀ F .fst = πᶠ E F∘ F
  Functors→Liftings .F₀ F .snd = ∫Functor→Lifting F

  Functors→Liftings .F₁ α .hom       = ∫Nat→Nat α
  Functors→Liftings .F₁ α .preserves = ∫Nat→Nat-lift α

  Functors→Liftings .F-id = total-hom-path Liftings
    (Nat-path  _  refl))
    (Nat-lift-pathp  _  refl))
  Functors→Liftings .F-∘ f g = total-hom-path Liftings
    (Nat-path  _  refl))
    (Nat-lift-pathp  _  refl))

This functor has a remarkably strict inverse, regardless of univalence of the fibrations and/or categories involved. It’s almost definitionally an isomorphism: because of our lack of η\eta-laws, we must explicitly appeal to some extensionality lemmas.

  Functors→Liftings-is-iso : is-precat-iso Functors→Liftings
  Functors→Liftings-is-iso .is-precat-iso.has-is-ff =
    is-iso→is-equiv $
      iso  α  Nat+Nat-lift→∫Nat (α .hom) (α .preserves))
       _  total-hom-path Liftings
        (Nat-path       λ _  refl)
        (Nat-lift-pathp λ _  refl))
       _  Nat-path  _  total-hom-path E refl refl))
  Functors→Liftings-is-iso .is-precat-iso.has-is-iso =
    is-iso→is-equiv $
      iso  F  Functor+Lifting→∫Functor (F .fst) (F .snd))
         _  Functor-path  _  refl)  _  refl) ,ₚ
               Lifting-pathp E _  _  refl)  _  refl))
         _  Functor-path  _  refl ,ₚ refl) λ _  refl)