{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- The canonical-map half of Lemma 2.3: the map D → D′ sending
-- (h, p₁ˢ, p₂ˢ) to (h, ι p₁ˢ, ι p₂ˢ, c) is an equivalence.
--
-- `buildD` is that map, in the notation of Extension.HomFillers.  The
-- h-component uses the canonical split presentation of the match of B → C Y
-- certified by `h-match-canonical`; the two path components are coercions of
-- the strict equalities; the coherence cell comes from strict-equality
-- induction, using that coercion commutes with ⁻¹, · and ap (the toolkit in
-- §1 below) and that parallel strict equalities agree by UIPᵉ.
--
-- `canonical-fill` is `buildD` read through the fibrant witness of D, and
-- `canonical-fillers-equiv` shows it is an equivalence, by composing it with
-- an explicitly invertible chain D′ ≃ ⟨D⟩ and using 2-out-of-3.
--------------------------------------------------------------------------------

module Extension.CanonicalFillers where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext using (is-cofib-2LTT)
open import Extension.Glue using (fibᵉ)
open import Extension.FundamentalId using (tot ; fiberwise-from-total)
open import Extension.HomFillers
  using ( tot-isEquiv ; concat-front-isEquiv ; inv-path-isEquiv
        ; fiber-htpy-equiv ; isEquiv-htpy ; isEquiv-left-cancel ; sing-collapse
        ; tr-inv-adj ; fiber-basept ; ap-pr1-dep-pair⁼ ; fiber-ap-pr1-equiv
        ; fiber-ap-pr1-equiv-β ; tr-cic ; tr-match-nat ; fib-≡
        ; module FibreLemmas ; module MatchedFibreEngine )
import Extension.HomFillers as HF

private
  variable
    ℓ ℓ' : Level

--------------------------------------------------------------------------------
-- §1  Strict-image paths: the coercion ι = cic-eq of strict equalities
-- commutes with the groupoid operations.  Each lemma is strict-equality
-- induction (matching on reflᵉ); at the base point both sides are refl.
--------------------------------------------------------------------------------

cic-eq-concat : {M : UU ℓ} {u v w : C M} (E₁ : u =ᵉ v) (E₂ : v =ᵉ w)
              → Id (cic-eq E₁ · cic-eq E₂) (cic-eq (exo-concat E₁ E₂))
cic-eq-concat reflᵉ reflᵉ = refl

cic-eq-inv : {M : UU ℓ} {u v : C M} (E : u =ᵉ v)
           → Id ((cic-eq E) ⁻¹) (cic-eq (exo-inv E))
cic-eq-inv reflᵉ = refl

ap-cic-eq : {M : UU ℓ} {N : UU ℓ'} (g : M → N) {u v : C M} (E : u =ᵉ v)
          → Id (ap g (cic-eq E)) (cic-eq (exo-ap (λ w → c (g (ic w))) E))
ap-cic-eq g reflᵉ = refl

-- coercion respects strict equality of strict equalities; with UIPᵉ this
-- makes any two parallel strict-image paths equal
cic-eq-cong : {M : UU ℓ} {u v : C M} {E E' : u =ᵉ v}
            → E =ᵉ E' → Id (cic-eq E) (cic-eq E')
cic-eq-cong reflᵉ = refl

cic-eq-irrel : {M : UU ℓ} {u v : C M} (E E' : u =ᵉ v)
             → Id (cic-eq E) (cic-eq E')
cic-eq-irrel E E' = cic-eq-cong (UIPᵉ E E')

--------------------------------------------------------------------------------
-- §2  The setting of Lemma 2.3, and the canonical map.
--------------------------------------------------------------------------------

module _ {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B}
         (cof2 : is-cofib-2LTT i ℓ)
         (cofA : isCofibrant A ℓ)
         (X : UU ℓ) (Z : X → UU ℓ)
         (l : A → C (Σ X Z)) (k : B → C X)
         (e₀ : (λ a → c (pr1 (ic (l a)))) =ᵉ (λ a → k (i a)))
  where

  open FibreLemmas X Z

  private
    -- the HomFillers section, instantiated
    D∙   = HF.D            cof2 cofA X Z l k e₀
    D′∙  = HF.D′           cof2 cofA X Z l k e₀
    WD   = HF.D-isFibrant  cof2 cofA X Z l k e₀
    MBX  = HF.MBX          cof2 cofA X Z l k e₀
    MAX  = HF.MAX          cof2 cofA X Z l k e₀
    SecB = HF.SecB         cof2 cofA X Z l k e₀
    SecA = HF.SecA         cof2 cofA X Z l k e₀
    ΣB   = HF.ΣB           cof2 cofA X Z l k e₀
    ΣA   = HF.ΣA           cof2 cofA X Z l k e₀
    P-A  = HF.P-A          cof2 cofA X Z l k e₀
    R-X  = HF.R-X          cof2 cofA X Z l k e₀
    R-Y  = HF.R-Y          cof2 cofA X Z l k e₀
    resSec = HF.resSec     cof2 cofA X Z l k e₀
    Lx   = HF.Lx           cof2 cofA X Z l k e₀
    l₂   = HF.l₂           cof2 cofA X Z l k e₀
    L∙   = HF.L∙           cof2 cofA X Z l k e₀
    K∙   = HF.K∙           cof2 cofA X Z l k e₀
    Ê    = HF.Ê            cof2 cofA X Z l k e₀
    f∘   = HF.f∘ᵖ          cof2 cofA X Z l k e₀
    tBX  = HF.tBXᵖ         cof2 cofA X Z l k e₀
    fBX  = HF.fBXᵖ         cof2 cofA X Z l k e₀
    ftBX = HF.ftBXᵖ        cof2 cofA X Z l k e₀
    tAX  = HF.tAXᵖ         cof2 cofA X Z l k e₀
    fAX  = HF.fAXᵖ         cof2 cofA X Z l k e₀
    tSecB = HF.tSecBᵖ      cof2 cofA X Z l k e₀
    fSecB = HF.fSecBᵖ      cof2 cofA X Z l k e₀
    ftSecB = HF.ftSecBᵖ    cof2 cofA X Z l k e₀
    tSecA = HF.tSecAᵖ      cof2 cofA X Z l k e₀
    ξ    = HF.ξᵖ           cof2 cofA X Z l k e₀
    ρ    = HF.ρᵖ           cof2 cofA X Z l k e₀
    l₂ᵉ  = HF.l₂ᵉᵖ         cof2 cofA X Z l k e₀
    Êᵉ   = HF.Êᵉᵖ          cof2 cofA X Z l k e₀
    GA   = HF.GAᵖ          cof2 cofA X Z l k e₀
    WSecA' = HF.WSecA'ᵖ    cof2 cofA X Z l k e₀

  ------------------------------------------------------------------------------
  -- The canonical coercion of a strict filler into a coherent homotopy filler.
  ------------------------------------------------------------------------------

  buildD : D∙ → D′∙
  buildD (h ,ᵉ (pˢ ,ᵉ qˢ)) = (m-h , s-h) , p₁ , p₂ , coh
    where
    -- the matched base f ∘ h ...
    m-h : MBX
    m-h = ic (tBX (λ b → f∘ (h b)))

    -- ... the strict realignment of the fibres of h onto it ...
    ξh : (b : B) → f∘ (h b) =ᵉ fBX (c m-h) b
    ξh b = exo-inv (happlyᵉ (ftBX (λ b' → f∘ (h b'))) b)

    sec-h : Πᵉ B (λ b → C (Z (ic (fBX (c m-h) b))))
    sec-h b = exo-tr CZic (ξh b) (c (pr2 (ic (h b))))

    -- ... and the matched fibre sections of h: the split presentation ⌜h⌝
    s-h : SecB m-h
    s-h = ic (tSecB m-h sec-h)

    -- ι p₂ˢ
    p₂ : Id m-h K∙
    p₂ = cic-eq (exo-ap tBX qˢ)

    -- ι p₁ˢ, base component: the strict equality of matched bases induced by
    -- pˢ : h ∘ i =ᵉ l (conjugated by the canonical realignments)
    SE : c (R-X m-h) =ᵉ c Lx
    SE = exo-ap tAX (funextᵉ (λ a →
           exo-concat (exo-inv (ξh (i a)))
                      (exo-ap (λ u → c (pr1 (ic u))) (happlyᵉ pˢ a))))

    base₁ : Id (R-X m-h) Lx
    base₁ = cic-eq SE

    -- ι p₁ˢ, fibre component: the strict transport of the matched fibre
    -- sections along SE agrees with ⌜l⌝'s fibre component (pure strict
    -- bookkeeping: pointwise transport collapse + fib-comp-cong along pˢ)
    E₂ : (a : A) → fAX (c (R-X m-h)) a =ᵉ fAX (c Lx) a
    E₂ a = exo-ap (λ w → fAX w a) SE

    BIG : (a : A) → c (pr1 (ic (h (i a)))) =ᵉ fAX (c Lx) a
    BIG a = exo-concat (ξh (i a)) (exo-concat (ξ m-h a) (E₂ a))

    sec-res : GA (c (R-X m-h))
    sec-res a = exo-tr CZic (ξ m-h a) (fSecB m-h (c s-h) (i a))

    SECEQ : exo-tr GA SE sec-res =ᵉ l₂ᵉ
    SECEQ = funextᵉ (λ a →
      exo-concat (exo-tr-pi SE (λ w a' → C (Z (ic (fAX w a')))))
     (exo-concat (exo-tr-ap' (λ w → fAX w a) SE)
     (exo-concat (exo-tr-elim {p = E₂ a}
                    (exo-tr-elim {p = ξ m-h a} (happlyᵉ (ftSecB m-h sec-h) (i a))))
     (exo-concat (exo-tr-concat (ξ m-h a) (E₂ a))
     (exo-concat (exo-tr-concat (ξh (i a)) (exo-concat (ξ m-h a) (E₂ a)))
                 (fib-comp-cong (happlyᵉ pˢ a) (BIG a) (ρ a)))))))

    FIB : Id (tr SecA base₁ (resSec m-h s-h)) l₂
    FIB = tr-cic (λ w → SecA (ic w)) SE (resSec m-h s-h)
          · cic-eq (exo-concat (tr-match-nat WSecA' SE sec-res)
                               (exo-ap (tSecA Lx) SECEQ))

    p₁ : Id (R-Y (m-h , s-h)) L∙
    p₁ = dep-pair⁼ (R-Y (m-h , s-h)) L∙ (base₁ , FIB)

    -- the strict-image form of ap R-X p₂
    RS : c (R-X m-h) =ᵉ c (R-X K∙)
    RS = exo-ap (λ w → c (R-X (ic w))) (exo-ap tBX qˢ)

    -- the coherence cell: all three legs are coercions of strict equalities,
    -- so the cell is UIPᵉ after pushing ι through ⁻¹, · and ap
    coh : Id ((ap P-A p₁ ⁻¹) · ap R-X p₂) Ê
    coh =
      ap (λ z → (z ⁻¹) · ap R-X p₂)
         (ap-pr1-dep-pair⁼ (R-Y (m-h , s-h)) L∙ (base₁ , FIB))
      · (ap (λ z → (base₁ ⁻¹) · z) (ap-cic-eq R-X (exo-ap tBX qˢ))
      · (ap (λ z → z · cic-eq RS) (cic-eq-inv SE)
      · (cic-eq-concat (exo-inv SE) RS
      · cic-eq-cong (UIPᵉ (exo-concat (exo-inv SE) RS) Êᵉ))))

  ------------------------------------------------------------------------------
  -- The canonical map on the fibrant match of D: pass through the fibrant
  -- witness back to a strict filler, then coerce.
  ------------------------------------------------------------------------------

  private
    toD : D∙ → C (fibrant-match WD)
    toD = pr1ᵉ (fibrant-witness WD)
    fromD : C (fibrant-match WD) → D∙
    fromD = pr1ᵉ (pr2ᵉ (fibrant-witness WD))

  canonical-fill : fibrant-match WD → D′∙
  canonical-fill d = buildD (fromD (c d))

--------------------------------------------------------------------------------
-- §3  Generic characterization lemmas for the legs of the HomFillers chain.
--
-- The chain of Lemma 2.3 contains three maps that do not compute
-- on general arguments: the forward map of `fiber-ap-pr1-equiv` (an `inv`),
-- the forward maps of the path-induction equivalences `tr-inv-adj` and
-- `fiber-basept`, and the (inverted) engine equivalence.  Each is characterized
-- here on the canonical elements produced by `buildD`: all path data on such
-- elements are coercions ι = `cic-eq` of strict equalities, so after
-- generalizing every strict equality in sight the characterizations are proved
-- by matching everything to reflᵉ (where both sides reduce to refl, or to an
-- instance of `inv-is-retraction`).
--------------------------------------------------------------------------------

private
  -- `ap` of the identity does nothing (propositionally)
  ap-id-refl : {A : UU ℓ} {x y : A} (r : Id x y) → Id r (ap (λ z → z) r)
  ap-id-refl refl = refl

-- transporting backwards then forwards along an inner path is the identity
tr-inv-section : {A : UU ℓ} (P : A → UU ℓ') {x y : A} (q : Id x y) (u : P y)
               → Id (tr P q (tr P (q ⁻¹) u)) u
tr-inv-section P refl u = refl

-- the forward map of `tr-inv-adj`, computed
tr-inv-adj-canonical : {A : UU ℓ} (P : A → UU ℓ') {x y : A} (q : Id x y)
                       (u : P y) (v : P x) (r : Id (tr P (q ⁻¹) u) v)
                     → Id (pr1 (tr-inv-adj P q u v) r)
                          ((tr-inv-section P q u ⁻¹) · ap (tr P q) r)
tr-inv-adj-canonical P refl u v r = ap-id-refl r

-- the forward map of `fiber-basept`, computed
fiber-basept-canonical : {A : UU ℓ} {B : UU ℓ'} (f : A → B) {b b' : B}
                         (p : Id b b') (w : fiber f b)
                       → Id (pr1 (fiber-basept f p) w) (pr1 w , pr2 w · p)
fiber-basept-canonical f refl w =
  ap (λ z → (pr1 w , z)) (right-unit (pr2 w) ⁻¹)

-- The forward map of `fiber-ap-pr1-equiv`, computed on the canonical fiber
-- element built by `buildD` (base path ι E, fibre path via `tr-cic`, coherence
-- cell the canonical strict-image cell).  All strict data are generalized;
-- matching them to reflᵉ reduces the element to the definitional image of the
-- backward map φ at refl, where the β-rule `fiber-ap-pr1-equiv-β` applies.
fap-canonical :
    {ℓm ℓq : Level} {M : UU ℓm} (Q : M → UU ℓq)
    (m₀ m₁ : C M) (E : m₀ =ᵉ m₁) (F : m₁ =ᵉ m₀)
    (s₀ : Q (ic m₀)) (t : C (Q (ic m₁)))
    (V : exo-tr (λ w → C (Q (ic w))) E (c s₀) =ᵉ t)
  → let u∙ = (ic m₀ , s₀)
        v∙ = (ic m₁ , ic t)
        FIB = tr-cic (λ w → Q (ic w)) E s₀ · cic-eq V
        P₁ = dep-pair⁼ u∙ v∙ (cic-eq E , FIB)
        coh' = ap (λ z → (z ⁻¹) · refl) (ap-pr1-dep-pair⁼ u∙ v∙ (cic-eq E , FIB))
             · (ap (λ z → z · refl) (cic-eq-inv E)
             · (cic-eq-concat (exo-inv E) reflᵉ
             · cic-eq-cong (UIPᵉ (exo-concat (exo-inv E) reflᵉ) F)))
        CM = (double-inv (ap pr1 P₁) ⁻¹)
           · ap (λ p → p ⁻¹) ((right-unit (ap pr1 P₁ ⁻¹) ⁻¹) · coh')
    in Id (pr1 (fiber-ap-pr1-equiv u∙ v∙ ((cic-eq F) ⁻¹)) (P₁ , CM))
          (ap (λ p → tr Q p s₀) (cic-eq-inv F · cic-eq-irrel (exo-inv F) E) · FIB)
fap-canonical Q m₀ .m₀ reflᵉ reflᵉ s₀ .(c s₀) reflᵉ =
  fiber-ap-pr1-equiv-β {P = Q} (ic m₀ , s₀) (ic m₀ , ic (c s₀)) refl refl

-- The two canonical composites out of a strict filler agree: the image of the
-- canonical fiber path under legs (ii)-(iv) of the chain equals the engine's
-- canonical fiber path.  Again all strict data are generalized and matched.
final-compare :
    {ℓm ℓq : Level} {M : UU ℓm} (Q : M → UU ℓq)
    (m₀ m₁ : C M) (E : m₀ =ᵉ m₁) (F : m₁ =ᵉ m₀)
    (z₀ : Q (ic m₀)) (t : C (Q (ic m₁)))
    (V : exo-tr (λ w → C (Q (ic w))) E (c z₀) =ᵉ t)
    (b∙ : C (Q (ic m₀)))
    (W : exo-tr (λ w → C (Q (ic w))) F t =ᵉ b∙)
    (u₁ : C (Q (ic m₀))) (Ea : c z₀ =ᵉ u₁) (Eb : u₁ =ᵉ b∙)
  → Id ( ( (tr-inv-section Q (cic-eq F) z₀ ⁻¹)
         · ap (tr Q (cic-eq F))
              ( ap (λ p → tr Q p z₀) (cic-eq-inv F · cic-eq-irrel (exo-inv F) E)
              · (tr-cic (λ w → Q (ic w)) E z₀ · cic-eq V) ) )
       · (tr-cic (λ w → Q (ic w)) F (ic t) · cic-eq W) )
       (cic-eq Ea · cic-eq Eb)
final-compare Q m₀ .m₀ reflᵉ reflᵉ z₀ .(c z₀) reflᵉ .(c z₀) reflᵉ .(c z₀) reflᵉ reflᵉ
  = refl

--------------------------------------------------------------------------------
-- §4  The engine leg: the forward map of `matched-fibre-equiv`, computed on
-- the match point of a strict fibre element.  The two components of the
-- resulting homotopy-fibre element are the match point of the strict fibre
-- element's point and its canonical strict-image path.
--------------------------------------------------------------------------------

module _ {ℓm : Level} {Eᵉ Fᵉ : UUᵉ ℓm}
         (g : Eᵉ → Fᵉ) (WF : isFibrant Fᵉ)
         (fibW : (p : Fᵉ) → isFibrant (fibᵉ g p))
         (ME : isFibrant Eᵉ)
         (ĝ : fibrant-match ME → fibrant-match WF)
         (Hc : (x : Eᵉ) → Id (ĝ (ic (pr1ᵉ (fibrant-witness ME) x)))
                             (ic (pr1ᵉ (fibrant-witness WF) (g x))))
  where

  private
    toF   = pr1ᵉ (fibrant-witness WF)
    fromF = pr1ᵉ (pr2ᵉ (fibrant-witness WF))
    ftF   = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WF)))
    tfF   = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WF)))
    toE   = pr1ᵉ (fibrant-witness ME)

    fmatch : Fᵉ → UU ℓm
    fmatch p = fibrant-match (fibW p)
    toFib : (p : Fᵉ) → fibᵉ g p → C (fmatch p)
    toFib p = pr1ᵉ (fibrant-witness (fibW p))
    fromFib : (p : Fᵉ) → C (fmatch p) → fibᵉ g p
    fromFib p = pr1ᵉ (pr2ᵉ (fibrant-witness (fibW p)))
    ftFib : (p : Fᵉ) (w : fibᵉ g p) → fromFib p (toFib p w) =ᵉ w
    ftFib p = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness (fibW p))))

    -- naturality of the to-match maps of the fibre witnesses (the engine's
    -- private `toFib-nat`, replicated)
    TN : {p q : Fᵉ} (e : p =ᵉ q) (w : fibᵉ g p)
       → exo-tr (λ p' → C (fmatch p')) e (toFib p w)
         =ᵉ toFib q (exo-tr (fibᵉ g) e w)
    TN reflᵉ w = reflᵉ

    -- moving a homotopy-fibre element along a strict equality of its
    -- strict-fibre representative: the path components are strict-image
    -- paths with shared head Hc, so UIPᵉ-irrelevance closes the comparison
    pm : (p₀ : Fᵉ) {x' x : Eᵉ} (SX : x' =ᵉ x)
         (E₁ : toF (g x') =ᵉ toF p₀) (E₂ : toF (g x) =ᵉ toF p₀)
       → Id {A = fiber ĝ (ic (toF p₀))}
            (ic (toE x') , Hc x' · cic-eq E₁)
            (ic (toE x)  , Hc x  · cic-eq E₂)
    pm p₀ {x' = x} reflᵉ E₁ E₂ =
      ap (λ z → (ic (toE x) , Hc x · z)) (cic-eq-irrel E₁ E₂)

  engine-canonical : (p₀ : Fᵉ) (w : fibᵉ g p₀)
    → Id (pr1 (MatchedFibreEngine.matched-fibre-equiv g WF fibW ME ĝ Hc p₀)
              (ic (toFib p₀ w)))
         (ic (toE (pr1ᵉ w)) , Hc (pr1ᵉ w) · cic-eq (exo-ap toF (pr2ᵉ w)))
  engine-canonical p₀ w = pm p₀ SX CC (exo-ap toF (pr2ᵉ w))
    where
    p' : Fᵉ
    p' = fromF (toF p₀)
    S* : C (fmatch p')
    S* = exo-tr (λ p'' → C (fmatch p'')) (exo-inv (ftF p₀)) (toFib p₀ w)
    w' : fibᵉ g p'
    w' = exo-tr (fibᵉ g) (exo-inv (ftF p₀)) w
    STEP : fromFib p' S* =ᵉ w'
    STEP = exo-concat (exo-ap (fromFib p') (TN (exo-inv (ftF p₀)) w))
                      (ftFib p' w')
    SX : pr1ᵉ (fromFib p' S*) =ᵉ pr1ᵉ w
    SX = exo-concat (exo-ap pr1ᵉ STEP) (pr1ᵉ-exo-tr-const (exo-inv (ftF p₀)) w)
    CC : toF (g (pr1ᵉ (fromFib p' S*))) =ᵉ toF p₀
    CC = exo-concat (exo-ap toF (pr2ᵉ (fromFib p' S*))) (tfF (c (ic (toF p₀))))

--------------------------------------------------------------------------------
-- §5  The chain computes the canonical map.
--
-- `key` below: for every strict filler d, the forward map of the HomFillers
-- chain sends the canonical homotopy filler `buildD d` to the match point
-- ⌜d⌝ of d.  Since the strict equalities pˢ, qˢ (and the strict commutativity
-- witness e₀ of the whole setting) can be matched to reflᵉ, l, k, e₀ are
-- quantified here, not fixed: it suffices to prove this at the strict point
--   l := h ∘ i,  k := f ∘ h,  e₀ := reflᵉ,  d := (h ,ᵉ (reflᵉ ,ᵉ reflᵉ)),
-- where the first two legs of the chain compute away (ι p₂ˢ ≡ refl) and the
-- remaining legs are handled by the §3/§4 characterizations.
--------------------------------------------------------------------------------

module _ {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B}
         (cof2 : is-cofib-2LTT i ℓ)
         (cofA : isCofibrant A ℓ)
         (X : UU ℓ) (Z : X → UU ℓ)
  where

  open FibreLemmas X Z

  module KeyStrict (h : B → C (Σ X Z)) where

    private
      l₀ : A → C (Σ X Z)
      l₀ a = h (i a)
      k₀ : B → C X
      k₀ b = c (pr1 (ic (h b)))

      -- the HomFillers section, instantiated at the strict point
      WD₀  = HF.D-isFibrant  cof2 cofA X Z l₀ k₀ reflᵉ
      MBX₀ = HF.MBX          cof2 cofA X Z l₀ k₀ reflᵉ
      SecA = HF.SecA         cof2 cofA X Z l₀ k₀ reflᵉ
      SecB = HF.SecB         cof2 cofA X Z l₀ k₀ reflᵉ
      R-X  = HF.R-X          cof2 cofA X Z l₀ k₀ reflᵉ
      resSec = HF.resSec     cof2 cofA X Z l₀ k₀ reflᵉ
      Lx   = HF.Lx           cof2 cofA X Z l₀ k₀ reflᵉ
      l₂   = HF.l₂           cof2 cofA X Z l₀ k₀ reflᵉ
      K∙   = HF.K∙           cof2 cofA X Z l₀ k₀ reflᵉ
      Ê    = HF.Ê            cof2 cofA X Z l₀ k₀ reflᵉ
      f∘   = HF.f∘ᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      tBX  = HF.tBXᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      fBX  = HF.fBXᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      ftBX = HF.ftBXᵖ        cof2 cofA X Z l₀ k₀ reflᵉ
      tAX  = HF.tAXᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      fAX  = HF.fAXᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      tSecB = HF.tSecBᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      fSecB = HF.fSecBᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      ftSecB = HF.ftSecBᵖ    cof2 cofA X Z l₀ k₀ reflᵉ
      tSecA = HF.tSecAᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      WSecA = HF.WSecAᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      WSecB = HF.WSecBᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      ξ    = HF.ξᵖ           cof2 cofA X Z l₀ k₀ reflᵉ
      ρ    = HF.ρᵖ           cof2 cofA X Z l₀ k₀ reflᵉ
      l₂ᵉ  = HF.l₂ᵉᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      Êᵉ   = HF.Êᵉᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      GA   = HF.GAᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      WSecA' = HF.WSecA'ᵖ    cof2 cofA X Z l₀ k₀ reflᵉ
      bd   = HF.bdᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      bridge = HF.bridgeᵖ    cof2 cofA X Z l₀ k₀ reflᵉ
      gK   = HF.gKᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      Y'   = HF.Y'ᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      bd'  = HF.bd'ᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      fibWK = HF.fibWKᵖ      cof2 cofA X Z l₀ k₀ reflᵉ
      HcK  = HF.HcKᵖ         cof2 cofA X Z l₀ k₀ reflᵉ
      ENG  = HF.engine-equivᵖ cof2 cofA X Z l₀ k₀ reflᵉ
      iso7 = HF.iso7ᵖ        cof2 cofA X Z l₀ k₀ reflᵉ
      e7   = HF.e7ᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      EB   = HF.EBᵖ          cof2 cofA X Z l₀ k₀ reflᵉ
      bnd-eq = HF.bnd-eqᵖ    cof2 cofA X Z l₀ k₀ reflᵉ
      CH   = HF.chainᵖ       cof2 cofA X Z l₀ k₀ reflᵉ
      Zk   = HF.Zk           cof2 cofA X Z l₀ k₀ reflᵉ
      l′   = HF.l′           cof2 cofA X Z l₀ k₀ reflᵉ
      SFE  = HF.strict-fillers-Ext cof2 cofA X Z l₀ k₀ reflᵉ
      cof  = HF.cof          cof2 cofA X Z l₀ k₀ reflᵉ

      -- the strict filler
      eD : HF.D cof2 cofA X Z l₀ k₀ reflᵉ
      eD = (h ,ᵉ (reflᵉ ,ᵉ reflᵉ))

      -- the components of `buildD eD` (replicated; definitionally the
      -- where-clauses of buildD at pˢ = qˢ = reflᵉ)
      m-h : MBX₀
      m-h = ic (tBX (λ b → f∘ (h b)))

      ξh : (b : B) → f∘ (h b) =ᵉ fBX (c m-h) b
      ξh b = exo-inv (happlyᵉ (ftBX (λ b' → f∘ (h b'))) b)

      sec-h : Πᵉ B (λ b → C (Z (ic (fBX (c m-h) b))))
      sec-h b = exo-tr CZic (ξh b) (c (pr2 (ic (h b))))

      s-h : SecB m-h
      s-h = ic (tSecB m-h sec-h)

      SE : c (R-X m-h) =ᵉ c Lx
      SE = exo-ap tAX (funextᵉ (λ a →
             exo-concat (exo-inv (ξh (i a)))
                        (exo-ap (λ u → c (pr1 (ic u)))
                                (happlyᵉ {f = l₀} {g = l₀} reflᵉ a))))

      E₂ : (a : A) → fAX (c (R-X m-h)) a =ᵉ fAX (c Lx) a
      E₂ a = exo-ap (λ w → fAX w a) SE

      BIG : (a : A) → c (pr1 (ic (h (i a)))) =ᵉ fAX (c Lx) a
      BIG a = exo-concat (ξh (i a)) (exo-concat (ξ m-h a) (E₂ a))

      sec-res : GA (c (R-X m-h))
      sec-res a = exo-tr CZic (ξ m-h a) (fSecB m-h (c s-h) (i a))

      SECEQ : exo-tr GA SE sec-res =ᵉ l₂ᵉ
      SECEQ = funextᵉ (λ a →
        exo-concat (exo-tr-pi SE (λ w a' → C (Z (ic (fAX w a')))))
       (exo-concat (exo-tr-ap' (λ w → fAX w a) SE)
       (exo-concat (exo-tr-elim {p = E₂ a}
                      (exo-tr-elim {p = ξ m-h a} (happlyᵉ (ftSecB m-h sec-h) (i a))))
       (exo-concat (exo-tr-concat (ξ m-h a) (E₂ a))
       (exo-concat (exo-tr-concat (ξh (i a)) (exo-concat (ξ m-h a) (E₂ a)))
                   (fib-comp-cong (happlyᵉ {f = l₀} {g = l₀} reflᵉ a)
                                  (BIG a) (ρ a)))))))

      VV : exo-tr (λ w → C (SecA (ic w))) SE (c (resSec m-h s-h)) =ᵉ c l₂
      VV = exo-concat (tr-match-nat WSecA' SE sec-res)
                      (exo-ap (tSecA Lx) SECEQ)

      -- the strict fibre element of the engine corresponding to h
      e₂' : (a : A) → fAX (c Lx) a =ᵉ fAX (c (R-X K∙)) a
      e₂' a = exo-ap (λ w → fAX w a) Êᵉ

      chA : (a : A) → bd a =ᵉ exo-tr CZic (exo-concat (ρ a) (e₂' a))
                                          (c (pr2 (ic (l₀ a))))
      chA a =
        exo-concat (exo-tr-pi Êᵉ (λ w a' → C (Z (ic (fAX w a')))))
        (exo-concat (exo-tr-ap' (λ w → fAX w a) Êᵉ)
                    (exo-tr-concat (ρ a) (e₂' a)))

      q-h : gK sec-h =ᵉ bd
      q-h = funextᵉ (λ a →
        exo-concat (exo-tr-concat (ξh (i a)) (ξ K∙ a))
        (exo-concat (exo-ap-tr (UIPᵉ (exo-concat (ξh (i a)) (ξ K∙ a))
                                     (exo-concat (ρ a) (e₂' a))))
                    (exo-inv (chA a))))

      w-h : fibᵉ gK bd
      w-h = (sec-h ,ᵉ q-h)

      x₀ : fibrant-match (fibWK bd)
      x₀ = ic (pr1ᵉ (fibrant-witness (fibWK bd)) w-h)

      -- the legs of the chain, named
      E7f : fibrant-match (fibWK bd) → fibrant-match WD₀
      E7f = pr1 e7
      EInv = pr1 (≃-sym ENG)
      FBf = pr1 (fiber-basept (resSec K∙) bridge)
      TrA = pr1 (tr-inv-adj SecA Ê (resSec K∙ s-h) l₂)

      -- the canonical fibre path produced by leg (ii)
      Y₀f : Id (tr SecA (Ê ⁻¹) (resSec K∙ s-h)) l₂
      Y₀f = ap (λ p → tr SecA p (resSec m-h s-h))
               (cic-eq-inv Êᵉ · cic-eq-irrel (exo-inv Êᵉ) SE)
          · (tr-cic (λ w → SecA (ic w)) SE (resSec m-h s-h) · cic-eq VV)

      Y₁f : Id (resSec K∙ s-h) (tr SecA Ê l₂)
      Y₁f = (tr-inv-section SecA Ê (resSec K∙ s-h) ⁻¹) · ap (tr SecA Ê) Y₀f

      -- steps (numbered by chain leg)
      step1 : Id (pr1 (fiber-ap-pr1-equiv (HF.R-Y cof2 cofA X Z l₀ k₀ reflᵉ (m-h , s-h))
                                          (HF.L∙ cof2 cofA X Z l₀ k₀ reflᵉ)
                                          (Ê ⁻¹))
                      ( dep-pair⁼ _ _ (cic-eq SE ,
                          tr-cic (λ w → SecA (ic w)) SE (resSec m-h s-h) · cic-eq VV)
                      , _ ))
                 Y₀f
      step1 = fap-canonical SecA (c (R-X m-h)) (c Lx) SE Êᵉ
                            (resSec m-h s-h) (c l₂) VV

      step2 : Id (TrA Y₀f) Y₁f
      step2 = tr-inv-adj-canonical SecA Ê (resSec K∙ s-h) l₂ Y₀f

      step3 : Id (FBf (s-h , Y₁f)) (s-h , Y₁f · bridge)
      step3 = fiber-basept-canonical (resSec K∙) bridge (s-h , Y₁f)

      Ea : c (resSec m-h s-h)
           =ᵉ tSecA (R-X K∙) (λ a → exo-tr CZic (ξ K∙ a) (sec-h (i a)))
      Ea = exo-ap (λ h' → tSecA (R-X K∙) (λ a → exo-tr CZic (ξ K∙ a) (h' (i a))))
                  (ftSecB K∙ sec-h)

      Eb : tSecA (R-X K∙) (λ a → exo-tr CZic (ξ K∙ a) (sec-h (i a)))
           =ᵉ tSecA (R-X K∙) bd
      Eb = exo-ap (tSecA (R-X K∙)) q-h

      stepFC : Id (Y₁f · bridge) (cic-eq Ea · cic-eq Eb)
      stepFC = final-compare SecA (c (R-X m-h)) (c Lx) SE Êᵉ
                             (resSec m-h s-h) (c l₂) VV
                             (tSecA (R-X K∙) bd)
                             (tr-match-nat WSecA' Êᵉ l₂ᵉ)
                             (tSecA (R-X K∙) (λ a → exo-tr CZic (ξ K∙ a) (sec-h (i a))))
                             Ea Eb

      step4 : Id {A = fiber (resSec K∙) (ic (tSecA (R-X K∙) bd))}
                 (s-h , Y₁f · bridge)
                 (pr1 ENG x₀)
      step4 = ap (λ z → (s-h , z)) stepFC
            · (engine-canonical gK (WSecA (R-X K∙)) fibWK (WSecB K∙)
                                (resSec K∙) HcK bd w-h) ⁻¹

      step5 : Id (EInv (pr1 ENG x₀)) x₀
      step5 = inv-is-retraction (pr1 ENG) (pr2 ENG) x₀

      -- step 6: the last leg e7 sends the engine point of h to ⌜eD⌝
      -- (pure strict bookkeeping through the match-equiv conjugation)
      wEY' = fibrant-witness (Ext-isFibrant cof Y' bd')
      tZk  = pr1ᵉ (fibrant-witness (Ext-isFibrant cof Zk l′))
      fromEY' = pr1ᵉ (pr2ᵉ wEY')
      ftEY'   = pr1ᵉ (pr2ᵉ (pr2ᵉ wEY'))
      rrfto = pr1ᵉ (HF.res-realign-fib-Ext CZic i
                      {u = λ b → fBX (c K∙) b}
                      {v = λ a → fAX (c (R-X K∙)) a}
                      (ξ K∙) bd)

      idpr : {a₁ a₂ : (a : A) → C (Zk (i a))} (E' : a₁ =ᵉ a₂)
             (w : Ext i (λ b → C (Zk b)) a₁)
           → pr1ᵉ (pr1ᵉ (idtoiso (exo-ap (Ext i (λ b → C (Zk b))) E')) w) =ᵉ pr1ᵉ w
      idpr reflᵉ w = reflᵉ

      E5d : (b : B) → exo-tr CZic (EB b) (sec-h b) =ᵉ c (pr2 (ic (h b)))
      E5d b = exo-concat (exo-tr-concat (ξh b) (EB b))
                         (exo-ap-tr (UIPᵉ (exo-concat (ξh b) (EB b)) reflᵉ))

      E5c : pr1ᵉ (pr1ᵉ iso7 (rrfto w-h)) =ᵉ pr1ᵉ (pr1ᵉ SFE eD)
      E5c = exo-concat
              (idpr bnd-eq
                (pr1ᵉ (HF.Ext-base-iso CZic i
                         {u = λ b → fBX (c K∙) b} {u' = k₀} EB bd')
                      (rrfto w-h)))
              (funextᵉ E5d)

      E5b : pr1ᵉ iso7 (rrfto w-h) =ᵉ pr1ᵉ SFE eD
      E5b = ext-≡ E5c

      step6 : Id (E7f x₀) (ic (pr1ᵉ (fibrant-witness WD₀) eD))
      step6 = cic-eq
        (exo-concat (exo-ap (λ w → tZk (pr1ᵉ iso7 w)) (ftEY' (rrfto w-h)))
                    (exo-ap tZk E5b))

    key-strict :
        Id (pr1 CH (buildD cof2 cofA X Z l₀ k₀ reflᵉ eD))
           (ic (pr1ᵉ (fibrant-witness WD₀) eD))
    key-strict =
        ap (λ y → E7f (EInv (FBf (s-h , TrA y)))) step1
      · (ap (λ y → E7f (EInv (FBf (s-h , y)))) step2
      · (ap (λ w → E7f (EInv w)) step3
      · (ap (λ w → E7f (EInv w)) step4
      · (ap E7f step5
      · step6))))

  -- the key lemma, for an arbitrary strict filler: strict-equality induction
  -- on pˢ, qˢ and the commutativity witness e₀ reduces to the strict point
  key : (h : B → C (Σ X Z))
        (l : A → C (Σ X Z)) (pˢ : (λ a → h (i a)) =ᵉ l)
        (k : B → C X)      (qˢ : (λ b → c (pr1 (ic (h b)))) =ᵉ k)
        (e₀ : (λ a → c (pr1 (ic (l a)))) =ᵉ (λ a → k (i a)))
      → Id (pr1 (HF.chainᵖ cof2 cofA X Z l k e₀)
                (buildD cof2 cofA X Z l k e₀ (h ,ᵉ (pˢ ,ᵉ qˢ))))
           (ic (pr1ᵉ (fibrant-witness (HF.D-isFibrant cof2 cofA X Z l k e₀))
                     (h ,ᵉ (pˢ ,ᵉ qˢ))))
  key h ._ reflᵉ ._ reflᵉ reflᵉ = KeyStrict.key-strict h

--------------------------------------------------------------------------------
-- §6  the canonical map of Lemma 2.3 is an equivalence.
--
-- The canonical map is an equivalence: composing it with the (equivalence)
-- forward chain of Lemma 2.3 is homotopic to the identity of
-- ⟨D⟩, by `key`, plus the section equation of the fibrant witness of D,
-- so 2-out-of-3 (`isEquiv-left-cancel`) applies.
--------------------------------------------------------------------------------

module _ {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B}
         (cof2 : is-cofib-2LTT i ℓ)
         (cofA : isCofibrant A ℓ)
         (X : UU ℓ) (Z : X → UU ℓ)
         (l : A → C (Σ X Z)) (k : B → C X)
         (e₀ : (λ a → c (pr1 (ic (l a)))) =ᵉ (λ a → k (i a)))
  where

  private
    WD  = HF.D-isFibrant cof2 cofA X Z l k e₀
    CH  = HF.chainᵖ      cof2 cofA X Z l k e₀
    fromD = pr1ᵉ (pr2ᵉ (fibrant-witness WD))
    tfD   = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WD)))

    -- the chain cancels the canonical map, pointwise
    H : (d : fibrant-match WD)
      → Id (pr1 CH (canonical-fill cof2 cofA X Z l k e₀ d)) d
    H d = key cof2 cofA X Z (pr1ᵉ dd) l (pr1ᵉ (pr2ᵉ dd)) k (pr2ᵉ (pr2ᵉ dd)) e₀
        · cic-eq (tfD (c d))
      where
      dd = fromD (c d)

  -- Lemma 2.3: the canonical strict-to-homotopy filler coercion
  -- is an equivalence of fibrant types
  canonical-fillers-equiv : isEquiv (canonical-fill cof2 cofA X Z l k e₀)
  canonical-fillers-equiv =
    isEquiv-left-cancel (canonical-fill cof2 cofA X Z l k e₀)
      (pr1 CH) (pr2 CH)
      (isEquiv-htpy (λ d → (H d) ⁻¹) id-is-equiv)

  -- packaged form
  canonical-fillers :
    fibrant-match WD ≃ HF.D′ cof2 cofA X Z l k e₀
  canonical-fillers =
    canonical-fill cof2 cofA X Z l k e₀ , canonical-fillers-equiv