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 displayed over contains the same data as a functor into 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 as in the following diagram:

If we unfold this in terms of displayed categories, such a lifting would give a diagram in lying over a corresponding diagram in

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 yield functors from to the total category of

  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 and let be their liftings along Furthermore, let be a natural transformation. A natural transformation of liftings between and over is given by a family of morphisms between and

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') (2 + n)
(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 via reindexing, we can use the existing cartesian lifts to build the lift of 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 is the functor category 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 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 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)