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}$, 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}$, 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}$-shaped diagram in $\mathcal{E}$ lying over a corresponding diagram in $\mathcal{B}$.

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[ F₀ (p i) x ]) (F' .F₀' x) (G' .F₀' x))
→ (∀ {x y} → (f : J.Hom x y)
→ PathP (λ i → Hom[ (F₁ (p i) 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}$.

  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}$, and let $F', G'$ be their liftings along $\pi : \mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}$. Furthermore, let $\alpha : F \to G$ be a natural transformation. A natural transformation of liftings between $F'$ and $G'$ over $\alpha$ is given by a family of morphisms $\eta_{j}$ between $F'(j)$ and $G'(j)$.

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

Nat-lift-is-set
: ∀ {F G : Functor J B} {F' : Lifting E F} {G' : Lifting E G}
→ {α : F => G} → is-set (F' =[ α ]=>l G')
Nat-lift-is-set =
(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$. 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}]$. 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 (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)