open import Cat.Displayed.Cartesian
open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
open import Cat.Displayed.Total
open import Cat.Functor.Compose
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Instances.Lifting where

open Functor
open _=>_
open Total-hom

Liftings🔗

A category $\mathcal{E}$ displayed over $\mathcal{B}$ contains the same data as a functor into $\mathcal{B}\text{,}$ 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:\mathcal{J}\to \mathcal{B}\text{,}$ as in the following diagram:

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

module _
  {o ℓ o' ℓ' oj ℓj}
  {B : Precategory o ℓ}
  {J : Precategory oj ℓj}
  (E : Displayed B o' ℓ')
  where
  private module J = Precategory J

  open Cat.Reasoning B
  open Displayed E
  open Cat.Displayed.Reasoning E

  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

  Lifting-pathp
    : {F G : Functor J B} {F' : Lifting F} {G' : Lifting G}
    → (p : F ≡ G)
    → (q : ∀ x → PathP (λ i → Ob[ p i .F₀ x ]) (F' .F₀' x) (G' .F₀' x))
    → (∀ {x y} → (f : J.Hom x y)
       → PathP (λ i → Hom[ p i .F₁ f ] (q x i) (q y i)) (F' .F₁' f) (G' .F₁' f))
    → PathP (λ i → Lifting (p i)) F' G'
  Lifting-pathp p q r i .F₀' x = q x i
  Lifting-pathp p q r i .F₁' f = r f i
  Lifting-pathp {F' = F'} {G' = G'} p q r i .F-id' {x} =
    is-set→squarep (λ i j → Hom[ (p i .F-id j) ]-set (q x i) (q x i))
      (r J.id)
      (F' .F-id')
      (G' .F-id')
      (λ _ → id') i
  Lifting-pathp {F' = F'} {G' = G'} p q r i .F-∘' {x} {y} {z} f g =
    is-set→squarep (λ i j → Hom[ p i .F-∘ f g j ]-set (q x i) (q z i))
      (r (f J.∘ g))
      (F' .F-∘' f g)
      (G' .F-∘' f g)
      (λ j → r f j ∘' r g j) i

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

  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:\mathcal{J}\to \mathcal{B}\text{,}$ and let $F^{\prime },G^{\prime }$ be their liftings along $\pi :\mathcal{E}\mathcal{B}\text{.}$ Furthermore, let $\alpha :F\to G$ be a natural transformation. A natural transformation of liftings between $F^{\prime }$ and $G^{\prime }$ over $\alpha$ is given by a family of morphisms ${\eta }_j$ between $F^{\prime }(j)$ and $G^{\prime }(j)\text{.}$

module _ {o ℓ o' ℓ' oj ℓj} {B : Precategory o ℓ} {J : Precategory oj ℓj} {E : Displayed B o' ℓ'} where
  private module J = Precategory J

  open Cat.Reasoning B
  open Displayed E
  open Cat.Displayed.Reasoning E
  open Lifting

  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

  open _=[_]=>l_

  Nat-lift-pathp
    : ∀ {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G}
    → {α : F => G} {β : F => G} {α' : F' =[ α ]=>l G'} {β' : F' =[ β ]=>l G'}
    → {p : α ≡ β}
    → (∀ j → α' .η' j ≡[ p ηₚ j ] β' .η' j)
    → PathP (λ i → F' =[ p i ]=>l G') α' β'
  Nat-lift-pathp q i .η' x = q x i
  Nat-lift-pathp {F' = F'} {G'} {α' = α'} {β'} {p = p} q i .is-natural' x y f =
    is-set→squarep (λ i j → Hom[ p i .is-natural x y f j ]-set _ _)
      (λ j → q y j ∘' F' .F₁' f)
      (α' .is-natural' x y f)
      (β' .is-natural' x y f)
      (λ j → G' .F₁' f ∘' q x j) i

  private unquoteDecl eqv = declare-record-iso eqv (quote _=[_]=>l_)

  instance
    H-Level-Nat-Lift
      : ∀ {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G} {α : F => G} {n}
      → H-Level (F' =[ α ]=>l G') ( + n)
    H-Level-Nat-Lift = basic-instance  $ Iso→is-hlevel!  eqv

Diagrammatically, 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 $F\to G$ is also a natural transformation $\pi \circ F^{\prime }\to \pi \circ G^{\prime }\text{;}$ showing this requires repacking some data due to the lack of some $\eta \text{-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 α' = ext λ _ → 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 $\mathcal{J}\to \mathcal{B}$ assemble into a displayed category over the functor category $[\mathcal{J},\mathcal{B}]\text{.}$ We shall denote this category ${\mathcal{E}}^{\mathcal{J}}\text{,}$ as it is the displayed analog of the fibration $\pi \circ -:{\mathcal{E}}^{\mathcal{J}}{\mathcal{B}}^{\mathcal{J}}\text{,}$ where $\pi :\mathcal{E}\mathcal{B}$ is a fibration.

module _
  {o ℓ o' ℓ' oj ℓj}
  {B : Precategory o ℓ}
  (E : Displayed B o' ℓ')
  (J : Precategory oj ℓj)
  where
  private module J = Precategory J

  open Cat.Reasoning B
  open Displayed E
  open Cat.Displayed.Reasoning E
  open Lifting
  open _=[_]=>l_

  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 _ _ _ = hlevel 
  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 $\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 $F\text{;}$ we can do this by reindexing $G^{\prime }$ 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 _ _))

    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 $G$ via reindexing, we can use the existing cartesian lifts to build the lift of $\alpha \text{.}$ 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 ${\mathcal{E}}^{\mathcal{J}}$ is the functor category $[\mathcal{J},\int \mathcal{E}]\text{.}$ 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.

  ∫Functor→Lifting F .F₀' j = F .F₀ j .snd
  ∫Functor→Lifting F .F₁' f = F .F₁ f .preserves
  ∫Functor→Lifting F .F-id' = cast[] (ap preserves (F .F-id))
  ∫Functor→Lifting F .F-∘' f g = cast[] (ap preserves (F .F-∘ f g))

  Functor+Lifting→∫Functor F F' .F₀ x .fst = F .F₀ x
  Functor+Lifting→∫Functor F F' .F₀ x .snd = F' .F₀' x
  Functor+Lifting→∫Functor F F' .F₁ f .hom = F .F₁ f
  Functor+Lifting→∫Functor F F' .F₁ f .preserves = F' .F₁' f
  Functor+Lifting→∫Functor F F' .F-id =
    total-hom-path E (F .F-id) (F' .F-id')
  Functor+Lifting→∫Functor F F' .F-∘ f g =
    total-hom-path E (F .F-∘ f g) (F' .F-∘' f g)

  ∫Nat→Nat α .η x = α .η x .hom
  ∫Nat→Nat α .is-natural x y f = ap hom (α .is-natural x y f)

  Nat+Nat-lift→∫Nat α α' .η x .hom = α .η x
  Nat+Nat-lift→∫Nat α α' .η x .preserves = α' .η' x
  Nat+Nat-lift→∫Nat α α' .is-natural x y f =
    total-hom-path E (α .is-natural x y f) (α' .is-natural' x y f)

  ∫Nat→Nat-lift α .η' x = α .η x .preserves
  ∫Nat→Nat-lift α .is-natural' x y f = ap preserves (α .is-natural x y f)

Using these repackagings, we can define the promised functor from $[\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 (ext λ _ → refl)
    (Nat-lift-pathp (λ _ → refl))
  Functors→Liftings .F-∘ f g = total-hom-path Liftings (ext (λ _ → 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 \text{-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
      (ext            λ _ → refl)
      (Nat-lift-pathp λ _ → refl))
    (λ _ → ext λ _ → 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)