Formalisation of the Symmetry Book - 26 descent

module synthetic-homotopy-theory.26-descent where

open import foundation.commuting-squares-of-maps
open import foundation.cones-over-cospans
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.pullbacks
open import foundation.sections
open import foundation.structure-identity-principle
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.universal-property-pushouts

Section 18.1 Five equivalent characterizations of pushouts

dep-cocone :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
dep-cocone {S = S} {A} {B} f g c P =
  Σ ( (a : A) → P ((pr1 c) a))
    ( λ hA →
      Σ ( (b : B) → P (pr1 (pr2 c) b))
        ( λ hB → (s : S) → Id (tr P (pr2 (pr2 c) s) (hA (f s))) (hB (g s))))

dep-cocone-map :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
  ( (x : X) → P x) → dep-cocone f g c P
dep-cocone-map f g c P h =
  ( λ a → h (pr1 c a)) ,
  ( λ b → h (pr1 (pr2 c) b)) ,
  ( λ s → apd h (pr2 (pr2 c) s))

Definition 18.1.1 The induction principle of pushouts

Ind-pushout :
  { l1 l2 l3 l4 : Level} (l : Level) →
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
Ind-pushout l {X = X} f g c =
  (P : X → UU l) → sec (dep-cocone-map f g c P)

Definition 18.1.2 The dependent universal property of pushouts

dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
dependent-universal-property-pushout l f g {X} c =
  (P : X → UU l) → is-equiv (dep-cocone-map f g c P)

Remark 18.1.3 Computation of the identity type of dep-cocone

We compute the identity type of dep-cocone in order to express the computation rules of the induction principle for pushouts.

coherence-htpy-dep-cocone :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  (P : X → UU l5) (c' c'' : dep-cocone f g c P)
  (K : (pr1 c') ~ (pr1 c'')) (L : (pr1 (pr2 c')) ~ (pr1 (pr2 c''))) →
  UU (l1 ⊔ l5)
coherence-htpy-dep-cocone {S = S} f g c P
  h h' K L =
  (s : S) →
  Id ( ((pr2 (pr2 h)) s) ∙ (L (g s)))
     ( (ap (tr P (pr2 (pr2 c) s)) (K (f s))) ∙ ((pr2 (pr2 h')) s))

htpy-dep-cocone :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  (s t : dep-cocone f g c P) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
htpy-dep-cocone {S = S} f g c P h h' =
  Σ ( (pr1 h) ~ (pr1 h')) (λ K →
    Σ ( (pr1 (pr2 h)) ~ (pr1 (pr2 h')))
      ( coherence-htpy-dep-cocone f g c P h h' K))

reflexive-htpy-dep-cocone :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  (s : dep-cocone f g c P) →
  htpy-dep-cocone f g c P s s
reflexive-htpy-dep-cocone f g (pair i (pair j H)) P
  (pair hA (pair hB hS)) =
  pair refl-htpy (pair refl-htpy right-unit-htpy)

htpy-dep-cocone-eq :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  {s t : dep-cocone f g c P} →
  Id s t → htpy-dep-cocone f g c P s t
htpy-dep-cocone-eq f g c P {s} {.s} refl =
  reflexive-htpy-dep-cocone f g c P s

abstract
  is-contr-total-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s : dep-cocone f g c P) →
    is-contr
      ( Σ (dep-cocone f g c P)
        ( htpy-dep-cocone f g c P s))
  is-contr-total-htpy-dep-cocone
    {S = S} {A} {B} f g {X} (pair i (pair j H)) P (pair hA (pair hB hS)) =
    is-contr-total-Eq-structure
      ( λ α βγ K →
          Σ (hB ~ (pr1 βγ)) (λ L →
          coherence-htpy-dep-cocone f g
            ( pair i (pair j H)) P (pair hA (pair hB hS)) (pair α βγ) K L))
      ( is-contr-total-htpy hA)
      ( pair hA refl-htpy)
      ( is-contr-total-Eq-structure
        ( λ β γ L →
          coherence-htpy-dep-cocone f g
            ( pair i (pair j H))
            ( P)
            ( pair hA (pair hB hS))
            ( pair hA (pair β γ))
            ( refl-htpy)
            ( L))
        ( is-contr-total-htpy hB)
        ( pair hB refl-htpy)
        ( is-contr-equiv
          ( Σ ((s : S) → Id (tr P (H s) (hA (f s))) (hB (g s))) (λ γ → hS ~ γ))
          ( equiv-tot (equiv-concat-htpy inv-htpy-right-unit-htpy))
          ( is-contr-total-htpy hS)))

abstract
  is-equiv-htpy-dep-cocone-eq :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) → is-equiv (htpy-dep-cocone-eq f g c P {s} {t})
  is-equiv-htpy-dep-cocone-eq f g c P s =
    fundamental-theorem-id
      ( is-contr-total-htpy-dep-cocone f g c P s)
      ( λ t → htpy-dep-cocone-eq f g c P {s} {t})

  eq-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) →
      htpy-dep-cocone f g c P s t → Id s t
  eq-htpy-dep-cocone f g c P s t =
    map-inv-is-equiv (is-equiv-htpy-dep-cocone-eq f g c P s t)

  issec-eq-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
      (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) →
    ( ( htpy-dep-cocone-eq f g c P {s} {t}) ∘
      ( eq-htpy-dep-cocone f g c P s t)) ~ id
  issec-eq-htpy-dep-cocone f g c P s t =
    issec-map-inv-is-equiv
    ( is-equiv-htpy-dep-cocone-eq f g c P s t)

  isretr-eq-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) →
    ( ( eq-htpy-dep-cocone f g c P s t) ∘
      ( htpy-dep-cocone-eq f g c P {s} {t})) ~ id
  isretr-eq-htpy-dep-cocone f g c P s t =
    isretr-map-inv-is-equiv
      ( is-equiv-htpy-dep-cocone-eq f g c P s t)

ind-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  Ind-pushout l f g c → (P : X → UU l) →
  dep-cocone f g c P → (x : X) → P x
ind-pushout f g c ind-c P =
  pr1 (ind-c P)

compute-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  htpy-dep-cocone f g c P
    ( dep-cocone-map f g c P (ind-pushout f g c ind-c P h))
    ( h)
compute-pushout f g c ind-c P h =
  htpy-dep-cocone-eq f g c P (pr2 (ind-c P) h)

left-compute-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  ( a : A) → Id (ind-pushout f g c ind-c P h (pr1 c a)) (pr1 h a)
left-compute-pushout f g c ind-c P h =
  pr1 (compute-pushout f g c ind-c P h)

right-compute-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  ( b : B) → Id (ind-pushout f g c ind-c P h (pr1 (pr2 c) b)) (pr1 (pr2 h) b)
right-compute-pushout f g c ind-c P h =
  pr1 (pr2 (compute-pushout f g c ind-c P h))

path-compute-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  coherence-htpy-dep-cocone f g c P
    ( dep-cocone-map f g c P (ind-pushout f g c ind-c P h))
    ( h)
    ( left-compute-pushout f g c ind-c P h)
    ( right-compute-pushout f g c ind-c P h)
path-compute-pushout f g c ind-c P h =
  pr2 (pr2 (compute-pushout f g c ind-c P h))

abstract
  uniqueness-dependent-universal-property-pushout :
    { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
    ( f : S → A) (g : S → B) (c : cocone f g X)
    ( dup-c : dependent-universal-property-pushout l f g c) →
    ( P : X → UU l) ( h : dep-cocone f g c P) →
    is-contr
      ( Σ ((x : X) → P x) (λ k →
          htpy-dep-cocone f g c P (dep-cocone-map f g c P k) h))
  uniqueness-dependent-universal-property-pushout f g c dup-c P h =
    is-contr-is-equiv'
      ( fib (dep-cocone-map f g c P) h)
      ( tot (λ k → htpy-dep-cocone-eq f g c P))
      ( is-equiv-tot-is-fiberwise-equiv
        ( λ k → is-equiv-htpy-dep-cocone-eq f g c P
          ( dep-cocone-map f g c P k) h))
      ( is-contr-map-is-equiv (dup-c P) h)

Before we state the main theorem of this section, we also state a dependent version of the pullback property of pushouts.

cone-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  cone
    ( λ (h : (a : A) → P (i a)) → λ (s : S) → tr P (H s) (h (f s)))
    ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
    ( (x : X) → P x)
cone-dependent-pullback-property-pushout f g (pair i (pair j H)) P =
  pair
    ( λ h → λ a → h (i a))
    ( pair
      ( λ h → λ b → h (j b))
      ( λ h → eq-htpy (λ s → apd h (H s))))

dependent-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
dependent-pullback-property-pushout l {S} {A} {B} f g {X}
  (pair i (pair j H)) =
  (P : X → UU l) →
  is-pullback
    ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
    ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
    ( cone-dependent-pullback-property-pushout f g (pair i (pair j H)) P)

Theorem 18.1.4

The following properties are all equivalent:

1. universal-property-pushout
2. pullback-property-pushout
3. dependent-pullback-property-pushout
4. dependent-universal-property-pushout
5. Ind-pushout

We have already shown (1) ↔ (2). Therefore we will first show (3) ↔ (4) ↔ (5). Finally, we will show (2) ↔ (3). Here are the precise references to the proofs of those parts:

• Proof of (1) → (2): pullback-property-pushout-universal-property-pushout
• Proof of (2) → (1): universal-property-pushout-pullback-property-pushout
• Proof of (2) → (3): dependent-pullback-property-pullback-property-pushout
• Proof of (3) → (2): pullback-property-dependent-pullback-property-pushout
• Proof of (3) → (4): dependent-universal-property-dependent-pullback-property-pushout
• Proof of (4) → (3): dependent-pullback-property-dependent-universal-property-pushout
• Proof of (4) → (5): Ind-pushout-dependent-universal-property-pushout
• Proof of (5) → (4): dependent-universal-property-pushout-Ind-pushout

Proof of Theorem 18.1.4, (5) implies (4)

dependent-naturality-square :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f f' : (x : A) → B x)
  {x x' : A} (p : Id x x') {q : Id (f x) (f' x)} {q' : Id (f x') (f' x')} →
  Id ((apd f p) ∙ q') ((ap (tr B p) q) ∙ (apd f' p)) →
  Id (tr (λ y → Id (f y) (f' y)) p q) q'
dependent-naturality-square f f' refl {q} {q'} s =
  inv (s ∙ (right-unit ∙ (ap-id q)))

htpy-eq-dep-cocone-map :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ( H : Ind-pushout l f g c) { P : X → UU l} (h h' : (x : X) → P x) →
  Id (dep-cocone-map f g c P h) (dep-cocone-map f g c P h') → h ~ h'
htpy-eq-dep-cocone-map f g c ind-c {P} h h' p =
  ind-pushout f g c ind-c
    ( λ x → Id (h x) (h' x))
    ( pair
      ( pr1 (htpy-dep-cocone-eq f g c P p))
      ( pair
        ( pr1 (pr2 (htpy-dep-cocone-eq f g c P p)))
        ( λ s →
          dependent-naturality-square h h' (pr2 (pr2 c) s)
            ( pr2 (pr2 (htpy-dep-cocone-eq f g c P p)) s))))

dependent-universal-property-pushout-Ind-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ((l : Level) → Ind-pushout l f g c) →
  ((l : Level) → dependent-universal-property-pushout l f g c)
dependent-universal-property-pushout-Ind-pushout f g c ind-c l P =
  is-equiv-has-inverse
    ( ind-pushout f g c (ind-c l) P)
    ( pr2 (ind-c l P))
    ( λ h → eq-htpy (htpy-eq-dep-cocone-map f g c (ind-c l)
      ( ind-pushout f g c (ind-c l) P (dep-cocone-map f g c P h))
      ( h)
      ( pr2 (ind-c l P) (dep-cocone-map f g c P h))))

Proof of Theorem 18.1.4, (4) implies (5)

Ind-pushout-dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ((l : Level) → dependent-universal-property-pushout l f g c) →
  ((l : Level) → Ind-pushout l f g c)
Ind-pushout-dependent-universal-property-pushout f g c dup-c l P =
  pr1 (dup-c l P)

Proof of Theorem 18.1.4, (4) implies (3)

triangle-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  ( dep-cocone-map f g c P) ~
  ( ( tot (λ h → tot (λ h' → htpy-eq))) ∘
    ( gap
      ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
      ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
      ( cone-dependent-pullback-property-pushout f g c P)))
triangle-dependent-pullback-property-pushout f g (pair i (pair j H)) P h =
  eq-pair-Σ refl (eq-pair-Σ refl (inv (issec-eq-htpy (apd h ∘ H))))

dependent-pullback-property-dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ((l : Level) → dependent-universal-property-pushout l f g c) →
  ((l : Level) → dependent-pullback-property-pushout l f g c)
dependent-pullback-property-dependent-universal-property-pushout
  f g (pair i (pair j H)) I l P =
  let c = (pair i (pair j H)) in
  is-equiv-right-factor-htpy
    ( dep-cocone-map f g c P)
    ( tot (λ h → tot λ h' → htpy-eq))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( _∘ g)
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h → is-equiv-tot-is-fiberwise-equiv
        ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
    ( I l P)

Proof of Theorem 18.1.4, (4) implies (3)

dependent-universal-property-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  ((l : Level) → dependent-pullback-property-pushout l f g c) →
  ((l : Level) → dependent-universal-property-pushout l f g c)
dependent-universal-property-dependent-pullback-property-pushout
  f g (pair i (pair j H)) dpullback-c l P =
  let c = (pair i (pair j H)) in
  is-equiv-comp-htpy
    ( dep-cocone-map f g c P)
    ( tot (λ h → tot λ h' → htpy-eq))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( _∘ g)
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( dpullback-c l P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h → is-equiv-tot-is-fiberwise-equiv
        ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))

Proof of Theorem 18.1.4, (3) implies (2)

concat-eq-htpy :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
  (H : f ~ g) (K : g ~ h) → Id (eq-htpy (H ∙h K)) ((eq-htpy H) ∙ (eq-htpy K))
concat-eq-htpy {A = A} {B} {f} H K =
  ind-htpy f
    ( λ g H →
      ( h : (x : A) → B x) (K : g ~ h) →
      Id (eq-htpy (H ∙h K)) ((eq-htpy H) ∙ (eq-htpy K)))
    ( λ h K → ap (concat' f (eq-htpy K)) (inv (eq-htpy-refl-htpy _))) H _ K

tr-triv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A} (p : Id x y) (b : B) →
  Id (tr (λ a → B) p b) b
tr-triv refl b = refl

apd-triv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : Id x y) →
  Id (apd f p) (tr-triv p (f x) ∙ ap f p)
apd-triv f refl = refl

pullback-property-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  dependent-pullback-property-pushout l f g c →
  pullback-property-pushout l f g c
pullback-property-dependent-pullback-property-pushout
  l f g (pair i (pair j H)) dpb Y =
  is-pullback-htpy
    -- ( λ h s → tr (λ x → Y) (H s) (h (f s)))
    ( λ h → eq-htpy (λ s → inv (tr-triv (H s) (h (f s)))))
    -- ( _∘ g)
    ( refl-htpy)
    { c = pair
      ( _∘ i)
      ( pair (_∘ j) (λ h → eq-htpy (h ·l H)))}
    ( cone-dependent-pullback-property-pushout
      f g (pair i (pair j H)) (λ x → Y))
    ( pair
      ( λ h → refl)
      ( pair
        ( λ h → refl)
        ( λ h → right-unit ∙
          ( ( ap eq-htpy
              ( eq-htpy (λ s →
                inv-con
                  ( tr-triv (H s) (h (i (f s))))
                  ( ap h (H s))
                  ( apd h (H s))
                  ( inv (apd-triv h (H s)))))) ∙
            ( concat-eq-htpy
              ( λ s → inv (tr-triv (H s) (h (i (f s)))))
              ( λ s → apd h (H s)))))))
    ( dpb (λ x → Y))

Proof of Theorem 18.1.4, (2) implies (3)

We first define the family of lifts, which is indexed by maps $Y\to X$.

fam-lifts :
  {l1 l2 l3 : Level} (Y : UU l1) {X : UU l2} (P : X → UU l3) →
  (Y → X) → UU (l1 ⊔ l3)
fam-lifts Y P h = (y : Y) → P (h y)

tr-fam-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) {f g : A → B} (H : f ~ g) →
  fam-lifts A P (h ∘ f) → fam-lifts A P (h ∘ g)
tr-fam-lifts' P h {f} {g} H k s = tr (P ∘ h) (H s) (k s)

TR-EQ-HTPY-FAM-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l4)
TR-EQ-HTPY-FAM-LIFTS {A = A} P h H =
  tr (fam-lifts A P) (eq-htpy (h ·l H)) ~ (tr-fam-lifts' P h H)

tr-eq-htpy-fam-lifts-refl-htpy :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) (f : A → B) → TR-EQ-HTPY-FAM-LIFTS P h (refl-htpy' f)
tr-eq-htpy-fam-lifts-refl-htpy P h f k =
  ap (λ t → tr (fam-lifts _ P) t k) (eq-htpy-refl-htpy (h ∘ f))

abstract
  tr-eq-htpy-fam-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
    (h : B → X) {f g : A → B} (H : f ~ g) →
    TR-EQ-HTPY-FAM-LIFTS P h H
  tr-eq-htpy-fam-lifts P h {f} =
    ind-htpy f
      ( λ g H → TR-EQ-HTPY-FAM-LIFTS P h H)
      ( tr-eq-htpy-fam-lifts-refl-htpy P h f)

  compute-tr-eq-htpy-fam-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
    (h : B → X) (f : A → B) →
    Id ( tr-eq-htpy-fam-lifts P h (refl-htpy' f))
        ( tr-eq-htpy-fam-lifts-refl-htpy P h f)
  compute-tr-eq-htpy-fam-lifts P h f =
    compute-ind-htpy f
      ( λ g H → TR-EQ-HTPY-FAM-LIFTS P h H)
      ( tr-eq-htpy-fam-lifts-refl-htpy P h f)

One of the basic operations on lifts is precomposition by an ordinary function.

precompose-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) → (f : A → B) → (h : B → X) →
  (fam-lifts B P h) → (fam-lifts A P (h ∘ f))
precompose-lifts P f h h' a = h' (f a)

Given two homotopic maps, their precomposition functions have different codomains. However, there is a commuting triangle. We obtain this triangle by homotopy induction.

TRIANGLE-PRECOMPOSE-LIFTS :
  { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  ( P : X → UU l4) {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
TRIANGLE-PRECOMPOSE-LIFTS {A = A} {B} {X} P {f} {g} H =
  (h : B → X) →
    ( (tr (fam-lifts A P) (eq-htpy (h ·l H))) ∘ (precompose-lifts P f h)) ~
    ( precompose-lifts P g h)

triangle-precompose-lifts-refl-htpy :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) → TRIANGLE-PRECOMPOSE-LIFTS P (refl-htpy' f)
triangle-precompose-lifts-refl-htpy {A = A} P f h h' =
  tr-eq-htpy-fam-lifts-refl-htpy P h f (λ a → h' (f a))

triangle-precompose-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) {f g : A → B} (H : f ~ g) →
  TRIANGLE-PRECOMPOSE-LIFTS P H
triangle-precompose-lifts {A = A} P {f} =
  ind-htpy f
    ( λ g H → TRIANGLE-PRECOMPOSE-LIFTS P H)
    ( triangle-precompose-lifts-refl-htpy P f)

compute-triangle-precompose-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) →
  Id
    ( triangle-precompose-lifts P (refl-htpy' f))
    ( triangle-precompose-lifts-refl-htpy P f)
compute-triangle-precompose-lifts P f =
  compute-ind-htpy f
    ( λ g → TRIANGLE-PRECOMPOSE-LIFTS P)
    ( triangle-precompose-lifts-refl-htpy P f)

There is a similar commuting triangle with the computed transport function. This time we don't use homotopy induction to construct the homotopy. We give an explicit definition instead.

triangle-precompose-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) {f g : A → B} (H : f ~ g) → (h : B → X) →
  ( (tr-fam-lifts' P h H) ∘ (precompose-lifts P f h)) ~
  ( precompose-lifts P g h)
triangle-precompose-lifts' P H h k = eq-htpy (λ a → apd k (H a))

compute-triangle-precompose-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) → (h : B → X) →
  ( triangle-precompose-lifts' P (refl-htpy' f) h) ~
  ( refl-htpy' ( precompose-lifts P f h))
compute-triangle-precompose-lifts' P f h k = eq-htpy-refl-htpy _

There is a coherence between the two commuting triangles. This coherence is again constructed by homotopy induction.

COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS {A = A} {B} {X} P {f} {g} H =
  (h : B → X) →
    ( triangle-precompose-lifts P H h) ~
    ( ( ( tr-eq-htpy-fam-lifts P h H) ·r (precompose-lifts P f h)) ∙h
      ( triangle-precompose-lifts' P H h))

coherence-triangle-precompose-lifts-refl-htpy :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  (f : A → B) → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P (refl-htpy' f)
coherence-triangle-precompose-lifts-refl-htpy P f h =
  ( htpy-eq (htpy-eq (compute-triangle-precompose-lifts P f) h)) ∙h
  ( ( ( inv-htpy-right-unit-htpy) ∙h
      ( ap-concat-htpy
        ( λ h' → tr-eq-htpy-fam-lifts-refl-htpy P h f (λ a → h' (f a)))
        ( refl-htpy)
        ( triangle-precompose-lifts' P refl-htpy h)
        ( inv-htpy (compute-triangle-precompose-lifts' P f h)))) ∙h
    ( htpy-eq
      ( ap
        ( λ t →
          ( t ·r (precompose-lifts P f h)) ∙h
          ( triangle-precompose-lifts' P refl-htpy h))
        ( inv (compute-tr-eq-htpy-fam-lifts P h f)))))

abstract
  coherence-triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    {f g : A → B} (H : f ~ g) → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H
  coherence-triangle-precompose-lifts P {f} =
    ind-htpy f
      ( λ g H → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( coherence-triangle-precompose-lifts-refl-htpy P f)

  compute-coherence-triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    (f : A → B) →
      Id ( coherence-triangle-precompose-lifts P (refl-htpy' f))
          ( coherence-triangle-precompose-lifts-refl-htpy P f)
  compute-coherence-triangle-precompose-lifts P f =
    compute-ind-htpy f
      ( λ g H → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( coherence-triangle-precompose-lifts-refl-htpy P f)

total-lifts :
  {l1 l2 l3 : Level} (A : UU l1) {X : UU l2} (P : X → UU l3) →
  UU (l1 ⊔ l2 ⊔ l3)
total-lifts A {X} P = universally-structured-Π {A = A} {B = λ a → X} (λ a → P)

precompose-total-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) → (A → B) →
  total-lifts B P → total-lifts A P
precompose-total-lifts {A = A} P f =
  map-Σ
    ( λ h → (a : A) → P (h a))
    ( λ h → h ∘ f)
    ( precompose-lifts P f)

coherence-square-map-inv-distributive-Π-Σ :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) →
  coherence-square-maps
    ( precompose-total-lifts P f)
    ( map-inv-distributive-Π-Σ {A = B} {B = λ x → X} {C = λ x y → P y})
    ( map-inv-distributive-Π-Σ)
    ( λ h → h ∘ f)
coherence-square-map-inv-distributive-Π-Σ P f = refl-htpy

Our goal is now to produce a homotopy between precompose-total-lifts P f and precompose-total-lifts P g for homotopic maps f and g, and a coherence filling a cylinder.

HTPY-PRECOMPOSE-TOTAL-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) {f g : A → B} (H : f ~ g) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
HTPY-PRECOMPOSE-TOTAL-LIFTS P {f} {g} H =
  (precompose-total-lifts P f) ~ (precompose-total-lifts P g)

htpy-precompose-total-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → HTPY-PRECOMPOSE-TOTAL-LIFTS P H
htpy-precompose-total-lifts {A = A} {B} P {f} {g} H =
  htpy-map-Σ
    ( fam-lifts A P)
    ( λ h → eq-htpy (h ·l H))
    ( precompose-lifts P f)
    ( triangle-precompose-lifts P H)

We show that when htpy-precompose-total-lifts is applied to refl-htpy, it computes to refl-htpy.

tr-id-left-subst :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {x y : A}
  (p : Id x y) (b : B) → (q : Id (f x) b) →
  Id (tr (λ (a : A) → Id (f a) b) p q) ((inv (ap f p)) ∙ q)
tr-id-left-subst refl b q = refl

compute-htpy-precompose-total-lifts :
  { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  ( f : A → B) →
  ( htpy-precompose-total-lifts P (refl-htpy {f = f})) ~
  ( refl-htpy' (map-Σ (fam-lifts A P) (λ h → h ∘ f) (precompose-lifts P f)))
compute-htpy-precompose-total-lifts {A = A} P f (pair h h') =
  let α = λ (t : Id (h ∘ f) (h ∘ f)) → tr (fam-lifts A P) t (λ a → h' (f a))
  in
  ap eq-pair-Σ'
    ( eq-pair-Σ
      ( eq-htpy-refl-htpy (h ∘ f))
      ( ( tr-id-left-subst
          { f = α}
          ( eq-htpy-refl-htpy (h ∘ f))
          ( λ a → h' (f a))
          ( triangle-precompose-lifts P refl-htpy h h')) ∙
        ( ( ap
            ( λ t → inv (ap α (eq-htpy-refl-htpy (λ a → h (f a)))) ∙ t)
            ( htpy-eq
              ( htpy-eq (compute-triangle-precompose-lifts P f) h) h')) ∙
          ( left-inv (triangle-precompose-lifts-refl-htpy P f h h')))))

COHERENCE-INV-HTPY-DISTRIBUTIVE-Π-Σ :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
COHERENCE-INV-HTPY-DISTRIBUTIVE-Π-Σ P {f} {g} H =
  ( ( coherence-square-map-inv-distributive-Π-Σ P f) ∙h
    ( map-inv-distributive-Π-Σ ·l ( htpy-precompose-total-lifts P H))) ~
  ( ( ( λ h → eq-htpy (h ·l H)) ·r map-inv-distributive-Π-Σ) ∙h
    ( coherence-square-map-inv-distributive-Π-Σ P g))

coherence-inv-htpy-distributive-Π-Σ-refl-htpy :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  (f : A → B) → COHERENCE-INV-HTPY-DISTRIBUTIVE-Π-Σ P (refl-htpy' f)
coherence-inv-htpy-distributive-Π-Σ-refl-htpy {X = X} P f =
  ( ap-concat-htpy
    ( coherence-square-map-inv-distributive-Π-Σ P f)
    ( map-inv-distributive-Π-Σ ·l ( htpy-precompose-total-lifts P refl-htpy))
    ( refl-htpy)
    ( λ h →
      ap
        ( ap map-inv-distributive-Π-Σ)
        ( compute-htpy-precompose-total-lifts P f h))) ∙h
  ( ap-concat-htpy'
    ( refl-htpy)
    ( ( htpy-precomp refl-htpy (Σ X P)) ·r map-inv-distributive-Π-Σ)
    ( refl-htpy)
    ( inv-htpy
      ( λ h → compute-htpy-precomp f (Σ X P) (map-inv-distributive-Π-Σ h))))

abstract
  coherence-inv-htpy-distributive-Π-Σ :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    {f g : A → B} (H : f ~ g) → COHERENCE-INV-HTPY-DISTRIBUTIVE-Π-Σ P H
  coherence-inv-htpy-distributive-Π-Σ P {f} =
    ind-htpy f
      ( λ g H → COHERENCE-INV-HTPY-DISTRIBUTIVE-Π-Σ P H)
      ( coherence-inv-htpy-distributive-Π-Σ-refl-htpy P f)

cone-family-dependent-pullback-property :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l) →
  cone-family
    ( fam-lifts S P)
    ( precompose-lifts P f)
    ( precompose-lifts P g)
    ( cone-pullback-property-pushout f g c X)
    ( fam-lifts X P)
cone-family-dependent-pullback-property f g c P γ =
  pair
    ( precompose-lifts P (pr1 c) γ)
    ( pair
      ( precompose-lifts P (pr1 (pr2 c)) γ)
      ( triangle-precompose-lifts P (pr2 (pr2 c)) γ))

is-pullback-cone-family-dependent-pullback-property :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ((l : Level) → pullback-property-pushout l f g c) →
  {l : Level} (P : X → UU l) (γ : X → X) →
  is-pullback
    ( ( tr (fam-lifts S P) (eq-htpy (γ ·l (pr2 (pr2 c))))) ∘
      ( precompose-lifts P f (γ ∘ (pr1 c))))
    ( precompose-lifts P g (γ ∘ (pr1 (pr2 c))))
    ( cone-family-dependent-pullback-property f g c P γ)
is-pullback-cone-family-dependent-pullback-property {S = S} {A} {B} {X}
  f g (pair i (pair j H)) pb-c P =
  let c = pair i (pair j H) in
  is-pullback-family-is-pullback-tot
    ( fam-lifts S P)
    ( precompose-lifts P f)
    ( precompose-lifts P g)
    ( cone-pullback-property-pushout f g c X)
    ( cone-family-dependent-pullback-property f g c P)
    ( pb-c _ X)
    ( is-pullback-top-is-pullback-bottom-cube-is-equiv
      ( precomp i (Σ X P))
      ( precomp j (Σ X P))
      ( precomp f (Σ X P))
      ( precomp g (Σ X P))
      ( map-Σ (fam-lifts A P) (precomp i X) (precompose-lifts P i))
      ( map-Σ (fam-lifts B P) (precomp j X) (precompose-lifts P j))
      ( map-Σ (fam-lifts S P) (precomp f X) (precompose-lifts P f))
      ( map-Σ (fam-lifts S P) (precomp g X) (precompose-lifts P g))
      ( map-inv-distributive-Π-Σ)
      ( map-inv-distributive-Π-Σ)
      ( map-inv-distributive-Π-Σ)
      ( map-inv-distributive-Π-Σ)
      ( htpy-precompose-total-lifts P H)
      ( refl-htpy)
      ( refl-htpy)
      ( refl-htpy)
      ( refl-htpy)
      ( htpy-precomp H (Σ X P))
      ( coherence-inv-htpy-distributive-Π-Σ P H)
      ( is-equiv-map-inv-distributive-Π-Σ)
      ( is-equiv-map-inv-distributive-Π-Σ)
      ( is-equiv-map-inv-distributive-Π-Σ)
      ( is-equiv-map-inv-distributive-Π-Σ)
      ( pb-c _ (Σ X P)))

dependent-pullback-property-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ((l : Level) → pullback-property-pushout l f g c) →
  ((l : Level) → dependent-pullback-property-pushout l f g c)
dependent-pullback-property-pullback-property-pushout
  {S = S} {A} {B} {X}
  f g (pair i (pair j H)) pullback-c l P =
  let c = pair i (pair j H) in
  is-pullback-htpy'
    -- ( (tr (fam-lifts S P) (eq-htpy (id ·l H))) ∘ (precompose-lifts P f i))
    ( (tr-eq-htpy-fam-lifts P id H) ·r (precompose-lifts P f i))
    -- ( precompose-lifts P g j)
    ( refl-htpy)
    ( cone-family-dependent-pullback-property f g c P id)
    { c' = cone-dependent-pullback-property-pushout f g c P}
    ( pair refl-htpy
      ( pair refl-htpy
        ( right-unit-htpy ∙h (coherence-triangle-precompose-lifts P H id))))
    ( is-pullback-cone-family-dependent-pullback-property f g c pullback-c P id)