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

--------------------------------------------------------------------------------
-- Lemma 2.3: strict fillers of a square against a fibration agree with the
-- coherent homotopy fillers.  I : A ↪ B is a full 2LTT cofibration, A is
-- cofibrant, and the fibration f : Y ↠ X with fibrant X is rendered as an
-- inner family Z over X with Y = Σ X Z and f = pr₁ (as in Extension.Fibre).
-- Cofibrancy of B is derived from CofibClosure, and only the fibration half
-- of the cofibration is used in the construction itself.
--
--   D  = Σᵉ (h : B → C Y). (h ∘ i =ᵉ l) ×ᵉ (f ∘ h =ᵉ k)
--   D′ = the coherent homotopy fillers, read through fibrant matches
--
-- `hom-fillers-equiv` is fibrant-match D-isFibrant ≃ D′.  Step 1 is
-- `strict-fillers-Ext`, D ≅ᵉ Extᵢ(Z ∘ k, l′), which is where fibrancy of D
-- comes from; D′ is an inner type by construction.  From there the equivalence
-- goes through singleton contractions and the fundamental theorem of identity
-- types, not through the pullback square and its Leibniz exponential as in the
-- paper; the two routes meet at the same extension type.
--------------------------------------------------------------------------------

module Extension.HomFillers where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext using (is-cofib-2LTT)
open import Extension.CofibClosure using (cofib-codomain-cofibrant)
open import Extension.Glue using (fibᵉ)
open import Extension.FundamentalId using (tot ; fiberwise-from-total)
open import Extension.RS412Ext using (match-equiv)
open import Extension.CanonicalFibre using (E-isFibrant)

private
  variable
    ℓ ℓ' ℓ'' : Level

--------------------------------------------------------------------------------
-- §1  Generic inner-HoTT helpers.
--------------------------------------------------------------------------------

-- The total map of a fibrewise equivalence is an equivalence.
tot-isEquiv : {A : UU ℓ} {P : A → UU ℓ'} {Q : A → UU ℓ''}
              (f : (a : A) → P a → Q a)
            → ((a : A) → isEquiv (f a)) → isEquiv (tot f)
tot-isEquiv {A = A} {P} {Q} f ef =
  invertibles-are-equiv (tot f) (tot g , η , ε)
  where
  g : (a : A) → Q a → P a
  g a = inv (f a) (ef a)
  η : (tot g ∘ tot f) ~ id
  η (a , p) = ap (λ z → (a , z)) (inv-is-retraction (f a) (ef a) p)
  ε : (tot f ∘ tot g) ~ id
  ε (a , q) = ap (λ z → (a , z)) (inv-is-section (f a) (ef a) q)

-- Pre-concatenation with a fixed path is an equivalence.
concat-front-isEquiv : {A : UU ℓ} {x y z : A} (ρ : Id x y)
                     → isEquiv (λ (r : Id y z) → ρ · r)
concat-front-isEquiv refl = id-is-equiv

-- Path inversion is an equivalence.
inv-path-isEquiv : {A : UU ℓ} {x y : A} → isEquiv (λ (p : Id x y) → p ⁻¹)
inv-path-isEquiv =
  invertibles-are-equiv (λ p → p ⁻¹) ((λ p → p ⁻¹) , double-inv , double-inv)

-- Fibres of homotopic maps are equivalent.
fiber-htpy-equiv : {A : UU ℓ} {B : UU ℓ'} {f g : A → B}
                   (H : (a : A) → Id (f a) (g a)) (b : B)
                 → fiber f b ≃ fiber g b
fiber-htpy-equiv {f = f} {g} H b =
  tot (λ a r → (H a ⁻¹) · r) ,
  tot-isEquiv (λ a r → (H a ⁻¹) · r) (λ a → concat-front-isEquiv (H a ⁻¹))

-- isEquiv is closed under homotopy.
isEquiv-htpy : {A : UU ℓ} {B : UU ℓ'} {f g : A → B}
               (H : (a : A) → Id (f a) (g a)) → isEquiv f → isEquiv g
isEquiv-htpy H ef b = is-contr-cong (fiber-htpy-equiv H b) (ef b)

-- 2-out-of-3, left cancellation: if h and h ∘ f are equivalences, so is f.
isEquiv-left-cancel : {A : UU ℓ} {B : UU ℓ'} {C' : UU ℓ''}
                      (f : A → B) (h : B → C')
                    → isEquiv h → isEquiv (h ∘ f) → isEquiv f
isEquiv-left-cancel f h eh ehf =
  isEquiv-htpy (λ a → inv-is-retraction h eh (f a))
               (∘-is-equiv (h ∘ f) (inv h eh) ehf (inv-is-equiv h eh))

-- Based-path collapse (singleton contraction with a dependent family).
sing-collapse : {A : UU ℓ} (a₀ : A) (T : (x : A) → Id x a₀ → UU ℓ')
              → Σ A (λ x → Σ (Id x a₀) (T x)) ≃ T a₀ refl
sing-collapse a₀ T = to' , invertibles-are-equiv to' (from' , η , ε)
  where
  to' : Σ _ (λ x → Σ (Id x a₀) (T x)) → T a₀ refl
  to' (x , refl , t) = t
  from' : T a₀ refl → Σ _ (λ x → Σ (Id x a₀) (T x))
  from' t = a₀ , refl , t
  η : (from' ∘ to') ~ id
  η (x , refl , t) = refl
  ε : (to' ∘ from') ~ id
  ε t = refl

-- Transport adjunction: paths out of a transport along q⁻¹ are paths into the
-- transport along q.
tr-inv-adj : {A : UU ℓ} (P : A → UU ℓ') {x y : A} (q : Id x y) (u : P y) (v : P x)
           → (Id (tr P (q ⁻¹) u) v) ≃ (Id u (tr P q v))
tr-inv-adj P refl u v = ≃-refl _

-- Fibres over identified base points are equivalent.
fiber-basept : {A : UU ℓ} {B : UU ℓ'} (f : A → B) {b b' : B}
             → Id b b' → fiber f b ≃ fiber f b'
fiber-basept f refl = ≃-refl _

-- ap pr1 computes on dep-pair⁼.
ap-pr1-dep-pair⁼ : {A : UU ℓ} {P : A → UU ℓ'} (u v : Σ A P) (w : dep-pair-Id u v)
                 → Id (ap (pr1 {B = P}) (dep-pair⁼ u v w)) (pr1 w)
ap-pr1-dep-pair⁼ (a , x) (a' , y) (refl , refl) = refl

-- The fibre of  ap pr₁ : Id u v → Id (pr₁ u) (pr₁ v)  over a base path q is
-- the type of paths between the transported second components.  This is the
-- engine behind "the coherence cell contracts to a single fibre path".
module _ {A : UU ℓ} {P : A → UU ℓ'} (u v : Σ A P) where

  private
    φ : (q : Id (pr1 u) (pr1 v))
      → Id (tr P q (pr2 u)) (pr2 v) → fiber (ap (pr1 {B = P}) {u} {v}) q
    φ q pz = dep-pair⁼ u v (q , pz) , ap-pr1-dep-pair⁼ u v (q , pz)

    contrL : Σ (Id (pr1 u) (pr1 v)) (λ q → fiber (ap (pr1 {B = P}) {u} {v}) q)
           → Id u v
    contrL (q , p₁ , r) = p₁

    contrL-isEquiv : isEquiv contrL
    contrL-isEquiv = invertibles-are-equiv contrL (contrL⁻¹ , η , ε)
      where
      contrL⁻¹ : Id u v → Σ (Id (pr1 u) (pr1 v)) (λ q → fiber (ap (pr1 {B = P}) {u} {v}) q)
      contrL⁻¹ p₁ = ap (pr1 {B = P}) p₁ , p₁ , refl
      η : (contrL⁻¹ ∘ contrL) ~ id
      η (q , p₁ , refl) = refl
      ε : (contrL ∘ contrL⁻¹) ~ id
      ε p₁ = refl

    contrR-isEquiv : isEquiv (λ (w : dep-pair-Id u v) → dep-pair⁼ u v w)
    contrR-isEquiv = invertibles-are-equiv _
      ( inv-dep-pair⁼ u v
      , htpy-inv-dep-pair⁼-dep-pair⁼ u v
      , htpy-dep-pair⁼-inv-dep-pair⁼ u v )

    totφ-isEquiv : isEquiv (tot φ)
    totφ-isEquiv = isEquiv-left-cancel (tot φ) contrL contrL-isEquiv
                     (isEquiv-htpy (λ w → refl) contrR-isEquiv)

    -- The fibrewise-equivalence witness is sealed with `abstract` so that
    -- applications of the ≃-sym'd forward map below stay neutral during
    -- conversion checking (they are `inv φ` applications, whose whnf would
    -- otherwise normalise the entire contractibility engine).  Nothing
    -- downstream needs this witness to unfold: it is a proof of a
    -- proposition, and the β-rule below is its computation interface.
    abstract
      φ-fibrewise-isEquiv : (q : Id (pr1 u) (pr1 v)) → isEquiv (φ q)
      φ-fibrewise-isEquiv = fiberwise-from-total φ totφ-isEquiv

  fiber-ap-pr1-equiv : (q : Id (pr1 u) (pr1 v))
                     → fiber (ap (pr1 {B = P}) {u} {v}) q
                       ≃ Id (tr P q (pr2 u)) (pr2 v)
  fiber-ap-pr1-equiv q = ≃-sym (φ q , φ-fibrewise-isEquiv q)

  -- β-rule: on canonically-built fiber elements the forward map computes.
  -- (Exported for Extension.CanonicalFillers, where the canonical
  -- strict-to-homotopy filler map is compared against the chain.)
  fiber-ap-pr1-equiv-β : (q : Id (pr1 u) (pr1 v)) (pz : Id (tr P q (pr2 u)) (pr2 v))
                       → Id (pr1 (fiber-ap-pr1-equiv q)
                              ( dep-pair⁼ u v (q , pz)
                              , ap-pr1-dep-pair⁼ u v (q , pz) ))
                            pz
  fiber-ap-pr1-equiv-β q pz =
    inv-is-retraction (φ q) (φ-fibrewise-isEquiv q) pz

--------------------------------------------------------------------------------
-- §2  Generic strict (exo) helpers.
--------------------------------------------------------------------------------

-- Transport of an ×ᵉ-pair splits componentwise.
tr-×ᵉ : {A : UUᵉ ℓ} {F : A → UUᵉ ℓ'} {G : A → UUᵉ ℓ''} {x y : A} (e : x =ᵉ y)
        (u : F x) (v : G x)
      → exo-tr (λ z → F z ×ᵉ G z) e (u ,ᵉ v) =ᵉ (exo-tr F e u ,ᵉ exo-tr G e v)
tr-×ᵉ reflᵉ u v = reflᵉ

-- Strict-fibre extensionality (second component is a strict proposition).
fib-≡ : {T S : UUᵉ ℓ} {e : T → S} {a : S} {w w' : fibᵉ e a}
      → pr1ᵉ w =ᵉ pr1ᵉ w' → w =ᵉ w'
fib-≡ {w = w} {w'} p = dep-pair-=ᵉ w w' (p ,ᵉ UIPᵉ _ _)

-- Transport along the coercion of a strict equality, in a family of matches
-- indexed through c.
tr-cic : {M : UU ℓ} (Q : C M → UU ℓ') {u v : C M} (E : u =ᵉ v) (z : Q u)
       → Id (tr (λ m → Q (c m)) (cic-eq E) z) (ic (exo-tr (λ w → C (Q w)) E (c z)))
tr-cic Q reflᵉ z = refl

-- Naturality of the to-match maps of a family of fibrancy witnesses.
tr-match-nat : {M : UU ℓ} {G : C M → UUᵉ ℓ'} (Wf : (w : C M) → isFibrant (G w))
               {u v : C M} (E : u =ᵉ v) (s : G u)
             → exo-tr (λ w → C (fibrant-match (Wf w))) E (pr1ᵉ (fibrant-witness (Wf u)) s)
               =ᵉ pr1ᵉ (fibrant-witness (Wf v)) (exo-tr G E s)
tr-match-nat Wf reflᵉ s = reflᵉ

--------------------------------------------------------------------------------
-- §3  Restriction-with-realignment and its strict fibres as extension types.
--------------------------------------------------------------------------------

module _ {ℓW ℓS ℓA : Level} {W : UUᵉ ℓW} (R : W → UUᵉ ℓA)
         {A B : UUᵉ ℓS} (i : A → B)
         {u : B → W} {v : A → W} (e : (a : A) → u (i a) =ᵉ v a)
  where

  -- restriction along i followed by pointwise strict realignment
  res-realign : ((b : B) → R (u b)) → ((a : A) → R (v a))
  res-realign h a = exo-tr R (e a) (h (i a))

  -- its strict fibre over p is an extension type (pure UIPᵉ/funextᵉ)
  res-realign-fib-Ext : (p : (a : A) → R (v a))
    → fibᵉ res-realign p
      ≅ Ext i (λ b → R (u b)) (λ a → exo-tr R (exo-inv (e a)) (p a))
  res-realign-fib-Ext p = to' ,ᵉ (from' ,ᵉ (ft' ,ᵉ tf'))
    where
    to' : fibᵉ res-realign p → Ext i (λ b → R (u b)) _
    to' (h ,ᵉ q) = h ,ᵉ funextᵉ (λ a → move-tr (e a) (happlyᵉ q a))
    from' : Ext i (λ b → R (u b)) _ → fibᵉ res-realign p
    from' (h ,ᵉ q) = h ,ᵉ funextᵉ (λ a → move-tr' (e a) (happlyᵉ q a))
    ft' : (w : fibᵉ res-realign p) → from' (to' w) =ᵉ w
    ft' w = fib-≡ reflᵉ
    tf' : (w : Ext i (λ b → R (u b)) _) → to' (from' w) =ᵉ w
    tf' w = ext-≡ reflᵉ

-- Transporting an extension type along a pointwise strict equality of the
-- base map (the family and the boundary move together).
module _ {ℓW ℓS ℓA : Level} {W : UUᵉ ℓW} (R : W → UUᵉ ℓA)
         {A B : UUᵉ ℓS} (i : A → B)
         {u u' : B → W} (E : (b : B) → u b =ᵉ u' b)
  where

  Ext-base-iso : (bd : (a : A) → R (u (i a)))
    → Ext i (λ b → R (u b)) bd
      ≅ Ext i (λ b → R (u' b)) (λ a → exo-tr R (E (i a)) (bd a))
  Ext-base-iso bd = to' ,ᵉ (from' ,ᵉ (ft' ,ᵉ tf'))
    where
    to' : Ext i (λ b → R (u b)) bd → Ext i (λ b → R (u' b)) _
    to' (h ,ᵉ q) =
      (λ b → exo-tr R (E b) (h b)) ,ᵉ
      funextᵉ (λ a → exo-tr-elim (happlyᵉ q a))
    from' : Ext i (λ b → R (u' b)) _ → Ext i (λ b → R (u b)) bd
    from' (h ,ᵉ q) =
      (λ b → exo-tr R (exo-inv (E b)) (h b)) ,ᵉ
      funextᵉ (λ a →
        exo-concat (exo-tr-elim (happlyᵉ q a))
        (exo-concat (exo-tr-concat (E (i a)) (exo-inv (E (i a))))
                    (exo-tr-right-law R (E (i a)))))
    ft' : (w : Ext i (λ b → R (u b)) bd) → from' (to' w) =ᵉ w
    ft' (h ,ᵉ q) = ext-≡ (funextᵉ (λ b →
      exo-concat (exo-tr-concat (E b) (exo-inv (E b)))
                 (exo-tr-right-law R (E b))))
    tf' : (w : Ext i (λ b → R (u' b)) _) → to' (from' w) =ᵉ w
    tf' (h ,ᵉ q) = ext-≡ (funextᵉ (λ b →
      exo-concat (exo-tr-concat (exo-inv (E b)) (E b))
                 (exo-tr-left-law R (E b))))

--------------------------------------------------------------------------------
-- §4  The matched-fibre engine.
--
-- A strengthening of Extension.CanonicalFibre: for a map g : E → F of exo
-- types with F fibrant and fibrewise-fibrant strict fibres, and for any
-- fibrancy witness ME of E together with any inner map ĝ between the matches
-- that renders g (hypothesis Hc, a homotopy against the match inclusions),
-- the match of the strict fibre of g over p₀ is canonically equivalent to the
-- homotopy fibre of ĝ over the match point of p₀.  (CanonicalFibre is the
-- special case where the match of E is the total space of the matched fibres
-- and ĝ is the projection.)  Proved by the same totalisation/2-out-of-3
-- scheme as CanonicalFibre, with the singleton contraction of the total
-- homotopy fibre replacing the definitional total-space computation.
--------------------------------------------------------------------------------

module MatchedFibreEngine
         {ℓ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
    matchF = fibrant-match WF
    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)))

    matchE = fibrant-match ME
    toE    = pr1ᵉ (fibrant-witness ME)
    fromE  = pr1ᵉ (pr2ᵉ (fibrant-witness ME))
    ftE    = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness ME)))
    tfE    = pr2ᵉ (pr2ᵉ (pr2ᵉ (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))))
    tfFib : (p : F) (x : C (fmatch p)) → toFib p (fromFib p x) =ᵉ x
    tfFib p = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness (fibW p))))

    -- naturality of toFib in the base point
    toFib-nat : {p q : F} (Ep : p =ᵉ q) (w : fibᵉ g p)
              → exo-tr (λ p' → C (fmatch p')) Ep (toFib p w)
                =ᵉ toFib q (exo-tr (fibᵉ g) Ep w)
    toFib-nat reflᵉ w = reflᵉ

    -- the two families over the match of F
    P1 : matchF → UU ℓm
    P1 m = fmatch (fromF (c m))
    P2 : matchF → UU ℓm
    P2 m = fiber ĝ m

    -- the canonical fibrewise coercion map
    κ : (m : matchF) → P1 m → P2 m
    κ m s =
      ic (toE x) ,
      (Hc x · cic-eq (exo-concat (exo-ap toF q) (tfF (c m))))
      where
      w = fromFib (fromF (c m)) (c s)
      x = pr1ᵉ w
      q = pr2ᵉ w

    -- total space of P1, and its identification with the match of E
    β' : Σ matchF P1 → matchE
    β' (m , s) = ic (toE (pr1ᵉ (fromFib (fromF (c m)) (c s))))

    β'⁻¹ : matchE → Σ matchF P1
    β'⁻¹ s = ic (toF (g x)) , ic (toFib p' w')
      where
      x  = fromE (c s)
      p' = fromF (toF (g x))
      w' : fibᵉ g p'
      w' = exo-tr (fibᵉ g) (exo-inv (ftF (g x))) (x ,ᵉ reflᵉ)

    β'-sect : (s : matchE) → Id (β' (β'⁻¹ s)) s
    β'-sect s = cic-eq (exo-concat (exo-ap toE step) (tfE (c s)))
      where
      x  = fromE (c s)
      p' = fromF (toF (g x))
      w' : fibᵉ g p'
      w' = exo-tr (fibᵉ g) (exo-inv (ftF (g x))) (x ,ᵉ reflᵉ)
      step : pr1ᵉ (fromFib p' (toFib p' w')) =ᵉ fromE (c s)
      step = exo-concat (exo-ap pr1ᵉ (ftFib p' w'))
                        (pr1ᵉ-exo-tr-const (exo-inv (ftF (g x))) (x ,ᵉ reflᵉ))

    β'-retr : (w : Σ matchF P1) → Id (β'⁻¹ (β' w)) w
    β'-retr (m , s) = dep-pair⁼ _ _ (p₁' , p₂')
      where
      pm : F
      pm = fromF (c m)
      w₀ : fibᵉ g pm
      w₀ = fromFib pm (c s)
      x₀ = pr1ᵉ w₀
      q₀ = pr2ᵉ w₀
      x' : E
      x' = fromE (toE x₀)
      p' = fromF (toF (g x'))
      w' : fibᵉ g p'
      w' = exo-tr (fibᵉ g) (exo-inv (ftF (g x'))) (x' ,ᵉ reflᵉ)

      E₁ : toF (g x') =ᵉ c m
      E₁ = exo-concat (exo-ap (λ t → toF (g t)) (ftE x₀))
           (exo-concat (exo-ap toF q₀) (tfF (c m)))

      p₁' : Id (ic (toF (g x'))) m
      p₁' = cic-eq E₁

      step3 : exo-tr (fibᵉ g) (exo-ap fromF E₁) w' =ᵉ w₀
      step3 = fib-≡
        (exo-concat (pr1ᵉ-exo-tr-const (exo-ap fromF E₁) w')
        (exo-concat (pr1ᵉ-exo-tr-const (exo-inv (ftF (g x'))) (x' ,ᵉ reflᵉ))
                    (ftE x₀)))

      E₂ : exo-tr (λ w'' → C (fmatch (fromF w''))) E₁ (toFib p' w') =ᵉ c s
      E₂ = exo-concat (exo-tr-ap' fromF E₁)
           (exo-concat (toFib-nat (exo-ap fromF E₁) w')
           (exo-concat (exo-ap (toFib pm) step3) (tfFib pm (c s))))

      p₂' : Id (tr P1 p₁' (ic (toFib p' w'))) s
      p₂' = tr-cic (λ w'' → fmatch (fromF w'')) E₁ (ic (toFib p' w')) · cic-eq E₂

    β'-isEquiv : isEquiv β'
    β'-isEquiv = invertibles-are-equiv β' (β'⁻¹ , β'-retr , β'-sect)

    -- singleton contraction of the total homotopy fibre
    contr2 : Σ matchF P2 → matchE
    contr2 (m , s , r) = s

    contr2-isEquiv : isEquiv contr2
    contr2-isEquiv = invertibles-are-equiv contr2 (contr2⁻¹ , η , ε)
      where
      contr2⁻¹ : matchE → Σ matchF P2
      contr2⁻¹ s = ĝ s , s , refl
      η : (contr2⁻¹ ∘ contr2) ~ id
      η (m , s , refl) = refl
      ε : (contr2 ∘ contr2⁻¹) ~ id
      ε s = refl

    -- 2-out-of-3: the totalisation of κ is an equivalence
    totκ-isEquiv : isEquiv (tot κ)
    totκ-isEquiv =
      isEquiv-left-cancel (tot κ) contr2 contr2-isEquiv
        (isEquiv-htpy (λ w → refl) β'-isEquiv)

    κ-isEquiv : (m : matchF) → isEquiv (κ m)
    κ-isEquiv = fiberwise-from-total κ totκ-isEquiv

    -- realignment of the fibre match along the round trip of the base point
    shift : {p q : F} (e : p =ᵉ q) → fmatch p → fmatch q
    shift e s = ic (exo-tr (λ p' → C (fmatch p')) e (c s))

    shift-isEquiv : {p q : F} (e : p =ᵉ q) → isEquiv (shift e)
    shift-isEquiv reflᵉ = id-is-equiv

    -- The equivalence witness of the engine's output is sealed with `abstract`
    -- so that applications of the backward map (`inv` of it, used by the
    -- ≃-sym'd leg of the HomFillers chain) stay neutral during conversion
    -- checking.  The forward map stays fully transparent; the
    -- witness is a proof of a proposition and never needs to unfold.
    abstract
      mfe-isEquiv : (p₀ : F)
        → isEquiv {A = fibrant-match (fibW p₀)}
                  {B = fiber ĝ (ic (pr1ᵉ (fibrant-witness WF) p₀))}
                  (λ s → κ (ic (toF p₀)) (shift (exo-inv (ftF p₀)) s))
      mfe-isEquiv p₀ =
        pr2 (≃-trans (shift (exo-inv (ftF p₀)) , shift-isEquiv (exo-inv (ftF p₀)))
                     (κ (ic (toF p₀)) , κ-isEquiv (ic (toF p₀))))

  -- The engine's output: the match of the strict fibre of g over p₀ is
  -- equivalent to the homotopy fibre of the matched map ĝ over ⌜p₀⌝.
  matched-fibre-equiv : (p₀ : F)
    → fibrant-match (fibW p₀) ≃ fiber ĝ (ic (pr1ᵉ (fibrant-witness WF) p₀))
  matched-fibre-equiv p₀ =
    (λ s → κ (ic (toF p₀)) (shift (exo-inv (ftF p₀)) s)) , mfe-isEquiv p₀

--------------------------------------------------------------------------------
-- §5  Fibrewise helpers for the family Z over X.
--------------------------------------------------------------------------------

module FibreLemmas {ℓ : Level} (X : UU ℓ) (Z : X → UU ℓ) where

  -- the coerced family over C X
  CZic : C X → UUᵉ ℓ
  CZic w = C (Z (ic w))

  -- moving the second component of a pair in C (Σ X Z) along a strict equality
  -- of first components
  pair-tr-lemma : {u v : C X} (E : u =ᵉ v) (z : CZic u)
                → c {A = Σ X Z} (ic u , ic z) =ᵉ c (ic v , ic (exo-tr CZic E z))
  pair-tr-lemma reflᵉ z = reflᵉ

  -- fibre components over strictly equal points, realigned to a common
  -- endpoint, agree (UIPᵉ)
  fib-comp-cong : {u v : C (Σ X Z)} (E : u =ᵉ v) {w : C X}
                  (q₁ : c (pr1 (ic u)) =ᵉ w) (q₂ : c (pr1 (ic v)) =ᵉ w)
                → exo-tr CZic q₁ (c (pr2 (ic u))) =ᵉ exo-tr CZic q₂ (c (pr2 (ic v)))
  fib-comp-cong reflᵉ q₁ q₂ = exo-ap-tr (UIPᵉ q₁ q₂)

--------------------------------------------------------------------------------
-- §6  Post-composition with the fibration, and the canonical splitting of the
--      match of the function space (S → C (Σ X Z)), [2LTT, Lem 3.9] one level
--      up.  Used both for the h-component of D′ and for its certification
--      `h-match-canonical`.
--------------------------------------------------------------------------------

module PostComp {ℓS ℓ : Level} (S : UUᵉ ℓS) (cofS : isCofibrant S ℓ)
                (X : UU ℓ) (Z : X → UU ℓ) where

  open FibreLemmas X Z

  -- post-composition with the fibration pr₁ : Σ X Z → X, coerced
  postcomp : (S → C (Σ X Z)) → (S → C X)
  postcomp h s = c (pr1 (ic (h s)))

  -- its strict fibre over p : S → C X is the space of sections of Z over p
  postfib-iso : (p : S → C X)
              → fibᵉ postcomp p ≅ Πᵉ S (λ s → C (Z (ic (p s))))
  postfib-iso p = to' ,ᵉ (from' ,ᵉ (ft' ,ᵉ tf'))
    where
    to' : fibᵉ postcomp p → Πᵉ S (λ s → C (Z (ic (p s))))
    to' (h ,ᵉ q) = λ s → exo-tr CZic (happlyᵉ q s) (c (pr2 (ic (h s))))
    from' : Πᵉ S (λ s → C (Z (ic (p s)))) → fibᵉ postcomp p
    from' t = (λ s → c (ic (p s) , ic (t s))) ,ᵉ reflᵉ
    ft' : (w : fibᵉ postcomp p) → from' (to' w) =ᵉ w
    ft' (h ,ᵉ q) = fib-≡ (funextᵉ (λ s →
      exo-inv (pair-tr-lemma (happlyᵉ q s) (c (pr2 (ic (h s)))))))
    tf' : (t : Πᵉ S (λ s → C (Z (ic (p s))))) → to' (from' t) =ᵉ t
    tf' t = reflᵉ

  -- the strict fibres of post-composition are fibrant, with match the match
  -- of the section space
  fibW-post : (p : S → C X) → isFibrant (fibᵉ postcomp p)
  fibW-post p = isFibrant-iso (≅-sym (postfib-iso p))
                              (Π-fibrant-witness (cofS (λ s → Z (ic (p s)))))

  private
    WSX = Π-fibrant-witness (cofS (λ _ → X))

  -- the canonical splitting: the match of (S → C (Σ X Z)) is the Σ, over the
  -- match of (S → C X), of the matches of the fibre-section spaces
  match-split :
    fibrant-match (Π-fibrant-witness (cofS (λ _ → Σ X Z)))
    ≃ Σ (fibrant-match WSX)
        (λ m → fibrant-match (Π-fibrant-witness
                 (cofS (λ s → Z (ic (pr1ᵉ (pr2ᵉ (fibrant-witness WSX)) (c m) s))))))
  match-split =
    match-equiv (Π-fibrant-witness (cofS (λ _ → Σ X Z)))
                (E-isFibrant WSX postcomp fibW-post)
                ≅-refl

--------------------------------------------------------------------------------
-- §7  The setting of Lemma 2.3.
--------------------------------------------------------------------------------

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

  -- the fibration half of the cofibration hypothesis ...
  cof : is-cofib i ℓ
  cof = pr1ᵉ cof2

  -- ... and cofibrancy of B, derived from the hypotheses as in the paper
  -- (Extension.CofibClosure).  `abstract` keeps the derived witness neutral
  -- during conversion checking; nothing below needs it to unfold.
  abstract
    cofB : isCofibrant B ℓ
    cofB = cofib-codomain-cofibrant cof2 cofA

  open FibreLemmas X Z

  private
    Y : UU ℓ
    Y = Σ X Z

    -- the fibration, coerced
    f∘ : C Y → C X
    f∘ w = c (pr1 (ic w))

  ------------------------------------------------------------------------------
  -- The type of strict fillers (the paper's D).
  ------------------------------------------------------------------------------

  D : UUᵉ (ℓS ⊔ ℓ)
  D = Σᵉ (B → C Y)
        (λ h → ((λ a → h (i a)) =ᵉ l) ×ᵉ ((λ b → f∘ (h b)) =ᵉ k))

  ------------------------------------------------------------------------------
  -- Step 1: D is strictly isomorphic to the extension
  -- type of the realigned boundary  l′  in the strict-fibre family  Z ∘ k.
  -- Pure UIPᵉ/funextᵉ bookkeeping.  This also gives fibrancy of D.
  ------------------------------------------------------------------------------

  Zk : B → UU ℓ
  Zk b = Z (ic (k b))

  l′ : (a : A) → C (Zk (i a))
  l′ a = exo-tr CZic (happlyᵉ e₀ a) (c (pr2 (ic (l a))))

  strict-fillers-Ext : D ≅ Ext i (λ b → C (Zk b)) l′
  strict-fillers-Ext = to' ,ᵉ (from' ,ᵉ (ft' ,ᵉ tf'))
    where
    to' : D → Ext i (λ b → C (Zk b)) l′
    to' (h ,ᵉ (p ,ᵉ q)) =
      (λ b → exo-tr CZic (happlyᵉ q b) (c (pr2 (ic (h b))))) ,ᵉ
      funextᵉ (λ a → fib-comp-cong (happlyᵉ p a) (happlyᵉ q (i a)) (happlyᵉ e₀ a))
    from' : Ext i (λ b → C (Zk b)) l′ → D
    from' (h ,ᵉ q) =
      (λ b → c (ic (k b) , ic (h b))) ,ᵉ
      ( funextᵉ (λ a →
          exo-concat (exo-ap (λ z → c (ic (k (i a)) , ic z)) (happlyᵉ q a))
                     (exo-inv (pair-tr-lemma (happlyᵉ e₀ a) (c (pr2 (ic (l a)))))))
      ,ᵉ reflᵉ )
    D-≡ : {d d' : D} → pr1ᵉ d =ᵉ pr1ᵉ d' → d =ᵉ d'
    D-≡ {d} {d'} p =
      dep-pair-=ᵉ d d'
        (p ,ᵉ exo-concat (tr-×ᵉ p (pr1ᵉ (pr2ᵉ d)) (pr2ᵉ (pr2ᵉ d)))
                         (pair-=ᵉ _ _ (UIPᵉ _ _ ,ᵉ UIPᵉ _ _)))
    ft' : (d : D) → from' (to' d) =ᵉ d
    ft' (h ,ᵉ (p ,ᵉ q)) = D-≡ (funextᵉ (λ b →
      exo-inv (pair-tr-lemma (happlyᵉ q b) (c (pr2 (ic (h b)))))))
    tf' : (w : Ext i (λ b → C (Zk b)) l′) → to' (from' w) =ᵉ w
    tf' (h ,ᵉ q) = ext-≡ reflᵉ

  -- D is fibrant, with fibrant match the match of the extension type.
  D-isFibrant : isFibrant D
  D-isFibrant = isFibrant-iso (≅-sym strict-fillers-Ext) (Ext-isFibrant cof Zk l′)

  ------------------------------------------------------------------------------
  -- The matched square: fibrant matches of the four function spaces and the
  -- matched renderings of  f ∘ −  and  − ∘ i.
  ------------------------------------------------------------------------------

  private
    WBX = Π-fibrant-witness (cofB (λ _ → X))
    WAX = Π-fibrant-witness (cofA (λ _ → X))

  -- ⟨B → X⟩ and ⟨A → X⟩
  MBX : UU (ℓS ⊔ ℓ)
  MBX = fibrant-match WBX
  MAX : UU (ℓS ⊔ ℓ)
  MAX = fibrant-match WAX

  private
    tBX = pr1ᵉ (fibrant-witness WBX)
    fBX = pr1ᵉ (pr2ᵉ (fibrant-witness WBX))
    ftBX = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WBX)))
    tAX = pr1ᵉ (fibrant-witness WAX)
    fAX = pr1ᵉ (pr2ᵉ (fibrant-witness WAX))
    ftAX = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WAX)))

    -- fibre-section witnesses over a matched base map
    WSecB : (m : MBX) → isFibrant (Πᵉ B (λ b → C (Z (ic (fBX (c m) b)))))
    WSecB m = Π-fibrant-witness (cofB (λ b → Z (ic (fBX (c m) b))))
    WSecA : (n : MAX) → isFibrant (Πᵉ A (λ a → C (Z (ic (fAX (c n) a)))))
    WSecA n = Π-fibrant-witness (cofA (λ a → Z (ic (fAX (c n) a))))

  -- matches of the fibre-section spaces
  SecB : MBX → UU (ℓS ⊔ ℓ)
  SecB m = fibrant-match (WSecB m)
  SecA : MAX → UU (ℓS ⊔ ℓ)
  SecA n = fibrant-match (WSecA n)

  private
    tSecB : (m : MBX) → Πᵉ B (λ b → C (Z (ic (fBX (c m) b)))) → C (SecB m)
    tSecB m = pr1ᵉ (fibrant-witness (WSecB m))
    fSecB : (m : MBX) → C (SecB m) → Πᵉ B (λ b → C (Z (ic (fBX (c m) b))))
    fSecB m = pr1ᵉ (pr2ᵉ (fibrant-witness (WSecB m)))
    ftSecB : (m : MBX) (h : Πᵉ B (λ b → C (Z (ic (fBX (c m) b)))))
           → fSecB m (tSecB m h) =ᵉ h
    ftSecB m = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness (WSecB m))))
    tSecA : (n : MAX) → Πᵉ A (λ a → C (Z (ic (fAX (c n) a)))) → C (SecA n)
    tSecA n = pr1ᵉ (fibrant-witness (WSecA n))

  -- ⟨B → Y⟩ and ⟨A → Y⟩, in the canonical split presentation of [2LTT, Lem 3.9]
  ΣB : UU (ℓS ⊔ ℓ)
  ΣB = Σ MBX SecB
  ΣA : UU (ℓS ⊔ ℓ)
  ΣA = Σ MAX SecA

  -- post-composition with f, matched: definitionally the projections
  P-B : ΣB → MBX
  P-B = pr1
  P-A : ΣA → MAX
  P-A = pr1

  -- restriction along i, matched, on the base ...
  R-X : MBX → MAX
  R-X m = ic (tAX (λ a → fBX (c m) (i a)))

  private
    -- ... with the strict realignment of the fibres it induces ...
    ξ : (m : MBX) (a : A) → fBX (c m) (i a) =ᵉ fAX (c (R-X m)) a
    ξ m a = exo-inv (happlyᵉ (ftAX (λ a' → fBX (c m) (i a'))) a)

  -- ... and on the fibre-sections
  resSec : (m : MBX) → SecB m → SecA (R-X m)
  resSec m s =
    ic (tSecA (R-X m) (λ a → exo-tr CZic (ξ m a) (fSecB m (c s) (i a))))

  -- restriction along i, matched, on ⟨B → Y⟩; note that
  --    P-A ∘ R-Y ≡ R-X ∘ P-B   holds definitionally
  -- (the match rendering of strict associativity f ∘ (h ∘ i) =ˢ (f ∘ h) ∘ i).
  R-Y : ΣB → ΣA
  R-Y (m , s) = R-X m , resSec m s

  ------------------------------------------------------------------------------
  -- The corners: ⌜l⌝ : ΣA, ⌜k⌝ : MBX, and the coercion e′ = Ê of the strict
  -- commutativity witness e₀.
  ------------------------------------------------------------------------------

  private
    fl : A → C X          -- f ∘ l, at the exo level
    fl a = f∘ (l a)

  Lx : MAX
  Lx = ic (tAX fl)

  private
    ρ : (a : A) → f∘ (l a) =ᵉ fAX (c Lx) a
    ρ a = exo-inv (happlyᵉ (ftAX fl) a)

    l₂ᵉ : Πᵉ A (λ a → C (Z (ic (fAX (c Lx) a))))
    l₂ᵉ a = exo-tr CZic (ρ a) (c (pr2 (ic (l a))))

  l₂ : SecA Lx
  l₂ = ic (tSecA Lx l₂ᵉ)

  -- ⌜l⌝ (the corner l, matched: its X-component and its fibre component)
  L∙ : ΣA
  L∙ = Lx , l₂

  -- ⌜k⌝
  K∙ : MBX
  K∙ = ic (tBX k)

  private
    -- the strict form of the coerced commutativity witness
    Êᵉ : tAX fl =ᵉ tAX (λ a → fBX (c K∙) (i a))
    Êᵉ = exo-ap tAX (funextᵉ (λ a →
           exo-concat (happlyᵉ e₀ a) (exo-inv (happlyᵉ (ftBX k) (i a)))))

  -- e′ ≔ ι(e₀), the coercion of the strict commutativity witness, transported
  -- into the matches by the canonical strict identifications
  Ê : Id (P-A L∙) (R-X K∙)
  Ê = cic-eq Êᵉ

  ------------------------------------------------------------------------------
  -- The type of coherent homotopy fillers (the paper's D′ in the
  -- match rendering; note (ap P-A p₁)⁻¹ · ap R-X p₂ is well-typed because
  -- P-A (R-Y h) ≡ R-X (P-B h) definitionally, strict associativity).
  ------------------------------------------------------------------------------

  D′ : UU (ℓS ⊔ ℓ)
  D′ = Σ ΣB (λ h →
       Σ (Id (R-Y h) L∙) (λ p₁ →
       Σ (Id (P-B h) K∙) (λ p₂ →
       Id ((ap P-A p₁ ⁻¹) · ap R-X p₂) Ê)))

  ------------------------------------------------------------------------------
  -- Certification of the h-component: ΣB is the fibrant match of the exo
  -- function space  B → C (Σ X Z)  (and likewise for ΣA), the two sides are
  -- the matches of the same exo type under two fibrancy witnesses, compared
  -- by the identity strict iso.
  ------------------------------------------------------------------------------

  h-match-canonical :
    fibrant-match (Π-fibrant-witness (cofB (λ _ → Σ X Z))) ≃ ΣB
  h-match-canonical = PostComp.match-split B cofB X Z

  hA-match-canonical :
    fibrant-match (Π-fibrant-witness (cofA (λ _ → Σ X Z))) ≃ ΣA
  hA-match-canonical = PostComp.match-split A cofA X Z

  ------------------------------------------------------------------------------
  -- The chain  D′ ≃ ⟨D⟩.
  ------------------------------------------------------------------------------

  private

    -- (i) reorder the components of D′
    T' : (m : MBX) → Id m K∙ → UU (ℓS ⊔ ℓ)
    T' m p₂ = Σ (SecB m) (λ s →
              Σ (Id (R-Y (m , s)) L∙) (λ p₁ →
              Id ((ap P-A p₁ ⁻¹) · ap R-X p₂) Ê))

    reorder-to : D′ → Σ MBX (λ m → Σ (Id m K∙) (T' m))
    reorder-to ((m , s) , p₁ , p₂ , z) = m , p₂ , s , p₁ , z

    reorder-from : Σ MBX (λ m → Σ (Id m K∙) (T' m)) → D′
    reorder-from (m , p₂ , s , p₁ , z) = (m , s) , p₁ , p₂ , z

    reorder-equiv : D′ ≃ Σ MBX (λ m → Σ (Id m K∙) (T' m))
    reorder-equiv =
      reorder-to ,
      invertibles-are-equiv reorder-to (reorder-from , η , ε)
      where
      η : (reorder-from ∘ reorder-to) ~ id
      η ((m , s) , p₁ , p₂ , z) = refl
      ε : (reorder-to ∘ reorder-from) ~ id
      ε (m , p₂ , s , p₁ , z) = refl

    -- (ii) the residual data over a strictly aligned  s : SecB K∙  collapses
    -- to a single path of fibre-sections
    cm : (s : SecB K∙) (p₁ : Id (R-Y (K∙ , s)) L∙)
       → Id ((ap P-A p₁ ⁻¹) · ap R-X (refl {x = K∙})) Ê
       → Id (ap (pr1 {B = SecA}) p₁) (Ê ⁻¹)
    cm s p₁ r =
      (double-inv (ap P-A p₁) ⁻¹) ·
      ap (λ p → p ⁻¹) ((right-unit (ap P-A p₁ ⁻¹) ⁻¹) · r)

    cm-isEquiv : (s : SecB K∙) (p₁ : Id (R-Y (K∙ , s)) L∙) → isEquiv (cm s p₁)
    cm-isEquiv s p₁ =
      ∘-is-equiv _ _
        (∘-is-equiv _ _
          (concat-front-isEquiv (right-unit (ap P-A p₁ ⁻¹) ⁻¹))
          (ap-isEquiv ((λ p → p ⁻¹) , inv-path-isEquiv) _ _))
        (concat-front-isEquiv (double-inv (ap P-A p₁) ⁻¹))

    resid : (s : SecB K∙)
          → (Σ (Id (R-Y (K∙ , s)) L∙) (λ p₁ →
              Id ((ap P-A p₁ ⁻¹) · ap R-X (refl {x = K∙})) Ê))
            ≃ Id (resSec K∙ s) (tr SecA Ê l₂)
    resid s =
      ≃-trans (tot (cm s) , tot-isEquiv (cm s) (cm-isEquiv s))
      (≃-trans (fiber-ap-pr1-equiv (R-Y (K∙ , s)) L∙ (Ê ⁻¹))
               (tr-inv-adj SecA Ê (resSec K∙ s) l₂))

    -- (iii) the strict form of the transported base point
    GA : C MAX → UUᵉ (ℓS ⊔ ℓ)
    GA w = Πᵉ A (λ a → C (Z (ic (fAX w a))))

    WSecA' : (w : C MAX) → isFibrant (GA w)
    WSecA' w = Π-fibrant-witness (cofA (λ a → Z (ic (fAX w a))))

    bd : GA (tAX (λ a → fBX (c K∙) (i a)))
    bd = exo-tr GA Êᵉ l₂ᵉ

    bridge : Id (tr SecA Ê l₂) (ic (tSecA (R-X K∙) bd))
    bridge =
      tr-cic (λ w → fibrant-match (WSecA' w)) Êᵉ l₂ ·
      cic-eq (tr-match-nat WSecA' Êᵉ l₂ᵉ)

    -- (iv) the engine instance: the matched restriction of fibre-sections
    gK : Πᵉ B (λ b → C (Z (ic (fBX (c K∙) b))))
       → Πᵉ A (λ a → C (Z (ic (fAX (c (R-X K∙)) a))))
    gK = res-realign CZic i (ξ K∙)

    Y' : B → UU ℓ
    Y' b = Z (ic (fBX (c K∙) b))

    bd' : (a : A) → C (Y' (i a))
    bd' a = exo-tr CZic (exo-inv (ξ K∙ a)) (bd a)

    fibWK : (p : Πᵉ A (λ a → C (Z (ic (fAX (c (R-X K∙)) a)))))
          → isFibrant (fibᵉ gK p)
    fibWK p =
      isFibrant-iso (≅-sym (res-realign-fib-Ext CZic i (ξ K∙) p))
        (Ext-isFibrant cof Y' (λ a → exo-tr CZic (exo-inv (ξ K∙ a)) (p a)))

    HcK : (x : Πᵉ B (λ b → C (Z (ic (fBX (c K∙) b)))))
        → Id (resSec K∙ (ic (pr1ᵉ (fibrant-witness (WSecB K∙)) x)))
             (ic (pr1ᵉ (fibrant-witness (WSecA (R-X K∙))) (gK x)))
    HcK x = cic-eq
      (exo-ap (λ h → tSecA (R-X K∙) (λ a → exo-tr CZic (ξ K∙ a) (h (i a))))
              (ftSecB K∙ x))

    module EngK = MatchedFibreEngine gK (WSecA (R-X K∙)) fibWK
                                     (WSecB K∙) (resSec K∙) HcK

    engine-equiv : fibrant-match (fibWK bd)
                 ≃ fiber (resSec K∙) (ic (tSecA (R-X K∙) bd))
    engine-equiv = EngK.matched-fibre-equiv bd

    -- (v) strict realignment: the engine's extension type is Extᵢ(Z ∘ k, l′)
    EB : (b : B) → fBX (c K∙) b =ᵉ k b
    EB b = happlyᵉ (ftBX k) b

    bnd-eq : (λ a → exo-tr CZic (EB (i a)) (bd' a)) =ᵉ l′
    bnd-eq = funextᵉ per-a
      where
      per-a : (a : A) → exo-tr CZic (EB (i a)) (bd' a) =ᵉ l′ a
      per-a a =
        exo-concat
          (exo-tr-elim {p = EB (i a)}
            (exo-concat
              (exo-tr-elim {p = exo-inv (ξ K∙ a)} chainA)
              (exo-tr-concat (exo-concat (ρ a) e₂) (exo-inv (ξ K∙ a)))))
        (exo-concat
          (exo-tr-concat
            (exo-concat (exo-concat (ρ a) e₂) (exo-inv (ξ K∙ a))) (EB (i a)))
          (exo-ap-tr (UIPᵉ _ (happlyᵉ e₀ a))))
        where
        z : CZic (f∘ (l a))
        z = c (pr2 (ic (l a)))
        e₂ : fAX (tAX fl) a =ᵉ fAX (tAX (λ a' → fBX (c K∙) (i a'))) a
        e₂ = exo-ap (λ w → fAX w a) Êᵉ
        chainA : bd a =ᵉ exo-tr CZic (exo-concat (ρ a) e₂) z
        chainA =
          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₂))

    iso7 : Ext i (λ b → C (Y' b)) bd' ≅ Ext i (λ b → C (Zk b)) l′
    iso7 = ≅-trans (Ext-base-iso CZic i EB bd')
                   (idtoiso (exo-ap (Ext i (λ b → C (Zk b))) bnd-eq))

    e7 : fibrant-match (fibWK bd) ≃ fibrant-match D-isFibrant
    e7 = match-equiv (Ext-isFibrant cof Y' bd') (Ext-isFibrant cof Zk l′) iso7

    -- (vi) the full chain
    chain : D′ ≃ fibrant-match D-isFibrant
    chain =
      ≃-trans reorder-equiv
      (≃-trans (sing-collapse K∙ T')
      (≃-trans (tot (λ s → pr1 (resid s)) ,
                tot-isEquiv (λ s → pr1 (resid s)) (λ s → pr2 (resid s)))
      (≃-trans (fiber-basept (resSec K∙) bridge)
      (≃-trans (≃-sym engine-equiv) e7))))

  ------------------------------------------------------------------------------
  -- Lemma 2.3: the strict fillers D and the coherent homotopy
  -- fillers D′ are both fibrant (D via `D-isFibrant`; D′ is an inner type by
  -- construction) and equivalent.
  ------------------------------------------------------------------------------

  hom-fillers-equiv : fibrant-match D-isFibrant ≃ D′
  hom-fillers-equiv = ≃-sym chain

  ------------------------------------------------------------------------------
  -- §8  Public aliases of internal components, consumed by
  -- Extension.CanonicalFillers (the canonical map of Lemma 2.3).  Each is
  -- definitionally the private component of the same name; they are exported
  -- so that the canonical strict-fillers → homotopy-fillers map can be
  -- written, and compared against the chain, outside this module.
  ------------------------------------------------------------------------------

  f∘ᵖ = f∘
  WBXᵖ = WBX
  WAXᵖ = WAX
  tBXᵖ = tBX
  fBXᵖ = fBX
  ftBXᵖ = ftBX
  tAXᵖ = tAX
  fAXᵖ = fAX
  ftAXᵖ = ftAX
  WSecBᵖ = WSecB
  WSecAᵖ = WSecA
  tSecBᵖ = tSecB
  fSecBᵖ = fSecB
  ftSecBᵖ = ftSecB
  tSecAᵖ = tSecA
  ξᵖ = ξ
  flᵖ = fl
  ρᵖ = ρ
  l₂ᵉᵖ = l₂ᵉ
  Êᵉᵖ = Êᵉ
  GAᵖ = GA
  WSecA'ᵖ = WSecA'
  bdᵖ = bd
  bridgeᵖ = bridge
  gKᵖ = gK
  Y'ᵖ = Y'
  bd'ᵖ = bd'
  fibWKᵖ = fibWK
  HcKᵖ = HcK
  engine-equivᵖ = engine-equiv
  iso7ᵖ = iso7
  e7ᵖ = e7
  EBᵖ = EB
  bnd-eqᵖ = bnd-eq
  chainᵖ = chain

{- References:

  [2LTT]       Danil Annenkov, Paolo Capriotti, Nicolai Kraus and Christian Sattler.
               Two-level type theory and applications.  Mathematical Structures in
               Computer Science 33(8):688-743, 2023.  doi:10.1017/s0960129523000130

-}