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

--------------------------------------------------------------------------------
-- Lemma 4.2: the constructor package inverts the restriction-unglue map
--
--   Θ : Π_Ψ G → Σ (t : Π_Φ T). Ext_i(A, f∙t),   Θ b = (b ∘ i via p, unglue ⊙ b).
--
-- Item (1), `package-to-inverse` and `inverse-to-package`: items (4)-(7) of
-- Definition 4.1 hold iff Θ has a strict two-sided inverse.  No cofibrancy.
--
-- Item (2), `Package2`: with unglue pointwise invertible, Θ is an equivalence,
-- by 2-out-of-3 against the projection κ and unglue ⊙ (-).  Products over a
-- cofibrant shape preserve fibrewise equivalences (`ProductEquiv`, using the
-- cofibrant-product funext of PiTruncation), and κ is an equivalence by the
-- matched fibre engine of HomFillers.  The constructor package then holds up
-- to homotopy, with a strict term boundary from RS 4.10, and is contractibly
-- unique as the homotopy fibre of Θ.
--
-- Item (3), `unglue-equiv-of-strict-inverse`: a strict two-sided inverse of Θ
-- makes unglue ⊙ (-) an equivalence, without pointwise invertibility.
--
-- Throughout, statements about Π_Ψ G and its kin are statements about the
-- fibrant matches, and "Θ is an equivalence" means that the matched rendering
-- Θ-hat is one.  Φ and Ψ live at a common level, as in HomFillers.
--------------------------------------------------------------------------------

module Extension.GlueConstructorPackage where

open import Extension.Prelude
open import Extension.Core
  using (Ext ; restrict ; ext-≡ ; pr1ᵉ-exo-tr-const ; exo-tr-ap')
open import Extension.CofibFibration using (is-cofib ; Ext-isFibrant ; i*)
open import Extension.GlueLiteralRules using (module GlueNotation)
open import Extension.GlueHomotopySemantic using (tr-inv-tr ; pairΣC-eq)
open import Extension.PiTruncation using (funext-Id-equiv)
open import Extension.RS410Pack using (HEP ; hep)
open import Extension.RelFunext using (rel-funext-holds)
open import Extension.RS412Ext using (match-equiv)
open import Extension.FundamentalId using (tot)
open import Extension.CanonicalFibre
  using (value-to-fiber ; value-to-fiber-isEquiv)
open import Extension.HomFillers
  using (module MatchedFibreEngine ; tot-isEquiv ; inv-path-isEquiv ;
         isEquiv-htpy ; isEquiv-left-cancel)

private
  variable
    ℓ ℓ' ℓ'' ℓφ ℓΨ ℓX ℓS 𝓤 : Level

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

-- Swapping two independent Σ-components.
swapΣ : {A : UU ℓ} {B : UU ℓ'} {R : A → B → UU ℓ''}
      → Σ A (λ a → Σ B (λ b → R a b)) ≃ Σ B (λ b → Σ A (λ a → R a b))
swapΣ {A = A} {B} {R} =
  sw , invertibles-are-equiv sw (sw' , (λ _ → refl) , (λ _ → refl))
  where
  sw : Σ A (λ a → Σ B (λ b → R a b)) → Σ B (λ b → Σ A (λ a → R a b))
  sw (x , y , r) = (y , x , r)
  sw' : Σ B (λ b → Σ A (λ a → R a b)) → Σ A (λ a → Σ B (λ b → R a b))
  sw' (y , x , r) = (x , y , r)

-- The projection of a Σ-type with contractible fibres is an equivalence.
pr1-contr-isEquiv : {A : UU ℓ} {P : A → UU ℓ'}
                  → ((a : A) → is-contr (P a)) → isEquiv (pr1 {B = P})
pr1-contr-isEquiv h a =
  is-contr-cong (value-to-fiber a , value-to-fiber-isEquiv a) (h a)

--------------------------------------------------------------------------------
-- §2  From pointwise paths to a path of matches (the backward direction of the
--     cofibrant-product funext `PiTruncation.funext-Id-equiv`).
--------------------------------------------------------------------------------

module MatchPath {ℓX 𝓤 : Level} {X : UUᵉ ℓX}
                 (cofX : isCofibrant X 𝓤) (Y : X → UU 𝓤) where

  private
    WY  = Π-fibrant-witness (cofX Y)
    tY  = pr1ᵉ (fibrant-witness WY)
    fY  = pr1ᵉ (pr2ᵉ (fibrant-witness WY))
    ftY = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WY)))

  match-of : ((x : X) → C (Y x)) → fibrant-match WY
  match-of g = ic (tY g)

  match-path-of-pointwise :
      (g₁ g₂ : (x : X) → C (Y x))
    → ((x : X) → Id (ic (g₁ x)) (ic (g₂ x)))
    → Id (match-of g₁) (match-of g₂)
  match-path-of-pointwise g₁ g₂ H =
    pr1 (≃-sym (funext-Id-equiv cofX Y g₁ (match-of g₂))) q
    where
    WId = Π-fibrant-witness
            (cofX (λ x → Id (ic (g₁ x)) (ic (fY (c (match-of g₂)) x))))
    q : fibrant-match WId
    q = ic (pr1ᵉ (fibrant-witness WId)
              (λ x → c (H x · cic-eq (exo-inv (happlyᵉ (ftY g₂) x)))))

--------------------------------------------------------------------------------
-- §3  Step A: products over cofibrant shapes preserve fibrewise equivalences.
--
-- Where the paper's Step A cites Lemma 3.13 (with Φ = ∅; funext for Π over the
-- cofibrant shape), we use the formalized product funext `funext-Id-equiv`
-- (through §2) and exhibit the matched pointwise inverse as a quasi-inverse.
--------------------------------------------------------------------------------

module ProductEquiv {ℓX 𝓤 : Level} {X : UUᵉ ℓX} (cofX : isCofibrant X 𝓤)
                    (B Y : X → UU 𝓤)
                    (v : (x : X) → B x → Y x)
                    (ev : (x : X) → C (isEquiv (v x)))
  where

  private
    WB  = Π-fibrant-witness (cofX B)
    tB  = pr1ᵉ (fibrant-witness WB)
    fB  = pr1ᵉ (pr2ᵉ (fibrant-witness WB))
    ftB = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WB)))
    tfB = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WB)))
    WY  = Π-fibrant-witness (cofX Y)
    tY  = pr1ᵉ (fibrant-witness WY)
    fY  = pr1ᵉ (pr2ᵉ (fibrant-witness WY))
    ftY = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WY)))
    tfY = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WY)))

  MB : UU (ℓX ⊔ 𝓤)
  MB = fibrant-match WB

  MY : UU (ℓX ⊔ 𝓤)
  MY = fibrant-match WY

  -- the fibrewise map and its pointwise inverse, on exo sections
  vΠ : ((x : X) → C (B x)) → ((x : X) → C (Y x))
  vΠ h x = c (v x (ic (h x)))

  wΠ : ((x : X) → C (Y x)) → ((x : X) → C (B x))
  wΠ g x = c (inv (v x) (ic (ev x)) (ic (g x)))

  -- the matched renderings
  v-match : MB → MY
  v-match m = ic (tY (vΠ (fB (c m))))

  w-match : MY → MB
  w-match m = ic (tB (wΠ (fY (c m))))

  private
    sect : (m : MY) → Id (v-match (w-match m)) m
    sect m =
      cic-eq (exo-ap (λ h → tY (vΠ h)) (ftB (wΠ g)))
      · (MatchPath.match-path-of-pointwise cofX Y (vΠ (wΠ g)) g
           (λ x → inv-is-section (v x) (ic (ev x)) (ic (g x)))
      · cic-eq (tfY (c m)))
      where
      g = fY (c m)

    retr : (m : MB) → Id (w-match (v-match m)) m
    retr m =
      cic-eq (exo-ap (λ g → tB (wΠ g)) (ftY (vΠ h)))
      · (MatchPath.match-path-of-pointwise cofX B (wΠ (vΠ h)) h
           (λ x → inv-is-retraction (v x) (ic (ev x)) (ic (h x)))
      · cic-eq (tfB (c m)))
      where
      h = fB (c m)

  -- Step A: the matched rendering of a fibrewise equivalence is an equivalence.
  v-match-isEquiv : isEquiv v-match
  v-match-isEquiv = invertibles-are-equiv v-match (w-match , retr , sect)

--------------------------------------------------------------------------------
-- §4  Item (1): the element-level rules are a strict two-sided inverse of Θ.
--     Purely formal, no cofibrancy, no fibrancy.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {𝓤 : Level}
         (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
         (G : Ψ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
         (ung : (ψ : Ψ) → G ψ → A ψ)
         (ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
                  exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
                         (λ ξ → c (pr1 (ic (f ξ)))) φ)
  where

  open GlueNotation i 𝓤 A T f G p ung ubd

  -- a strict two-sided inverse of the restriction-unglue map Θ
  StrictInverse : UUᵉ (ℓφ ⊔ ℓΨ ⊔ 𝓤)
  StrictInverse =
    Σᵉ (GlueInputTm → ((ψ : Ψ) → C (G ψ)))
       (λ Θ⁻¹ → ((b : (ψ : Ψ) → C (G ψ)) → Θ⁻¹ (Θ b) =ᵉ b)
             ×ᵉ ((w : GlueInputTm) → Θ (Θ⁻¹ w) =ᵉ w))

  -- items (4)-(7)  ⇒  strict two-sided inverse (which is glue itself)
  package-to-inverse : ConstructorPackage → StrictInverse
  package-to-inverse pkg =
      (λ w → glue (pr1ᵉ w) (pr2ᵉ w))
    ,ᵉ ((λ b → exo-inv (glue-η b)) ,ᵉ sect)
    where
    open ConstructorPackage pkg
    sect : (w : GlueInputTm) → Θ (glue (pr1ᵉ w) (pr2ᵉ w)) =ᵉ w
    sect (t ,ᵉ a) =
      dep-pair-=ᵉ _ _
        ( glue-bdry t a
        ,ᵉ ext-≡ (exo-concat
             (pr1ᵉ-exo-tr-const (glue-bdry t a) (unglue⊙ (glue t a)))
             (glue-β t a)) )

  -- strict two-sided inverse  ⇒  items (4)-(7)
  inverse-to-package : StrictInverse → ConstructorPackage
  inverse-to-package (Θ⁻¹ ,ᵉ (retr ,ᵉ sect)) = record
    { glue      = λ t a → Θ⁻¹ (t ,ᵉ a)
    ; glue-bdry = λ t a → exo-ap pr1ᵉ (sect (t ,ᵉ a))
    ; glue-η    = λ b → exo-inv (retr b)
    ; glue-β    = λ t a → exo-ap (λ w → pr1ᵉ (pr2ᵉ w)) (sect (t ,ᵉ a))
    }

--------------------------------------------------------------------------------
-- §5  An exo-J helper: converting pointwise paths through the type boundary.
--------------------------------------------------------------------------------

-- From pointwise paths between (b ∘ i via p) and t (in T) to pointwise paths
-- between (t via p⁻¹) and b ∘ i (in G).
tG-path-convert :
    {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {𝓤 : Level}
    (G : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
    (b : (ψ : Ψ) → C (G ψ)) (t : (φ : Φ) → C (T φ))
    (r : (φ : Φ) → Id (ic (exo-tr (λ H → (ξ : Φ) → C (H ξ)) p
                             (λ φ' → b (i φ')) φ))
                      (ic (t φ)))
    (φ : Φ)
  → Id (ic (exo-tr (λ H → (ξ : Φ) → C (H ξ)) (exo-inv p) t φ)) (ic (b (i φ)))
tG-path-convert i G .(λ φ → G (i φ)) reflᵉ b t r φ = (r φ) ⁻¹

--------------------------------------------------------------------------------
-- §6  The Θ analysis: Steps A-C, items (2) and (3).
--------------------------------------------------------------------------------

module ThetaAnalysis
    {ℓS 𝓤 : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
    (cof : is-cofib i 𝓤)
    (cofΦ : isCofibrant Φ 𝓤) (cofΨ : isCofibrant Ψ 𝓤)
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
    (G : Ψ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
    (ung : (ψ : Ψ) → G ψ → A ψ)
    (ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
             exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
                    (λ ξ → c (pr1 (ic (f ξ)))) φ)
  where

  open GlueNotation i 𝓤 A T f G p ung ubd

  private
    triv = rel-funext-holds cof cofΨ cofΦ

    Ai : Φ → UU 𝓤
    Ai φ = A (i φ)

    -- the four function-space witnesses
    WT  = Π-fibrant-witness (cofΦ T)
    WAF = Π-fibrant-witness (cofΦ Ai)
    WAS = Π-fibrant-witness (cofΨ A)
    WG  = Π-fibrant-witness (cofΨ G)

    tT   = pr1ᵉ (fibrant-witness WT)
    fT   = pr1ᵉ (pr2ᵉ (fibrant-witness WT))
    ftT  = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WT)))
    tfT  = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WT)))
    tAF  = pr1ᵉ (fibrant-witness WAF)
    fAF  = pr1ᵉ (pr2ᵉ (fibrant-witness WAF))
    ftAF = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WAF)))
    tAS  = pr1ᵉ (fibrant-witness WAS)
    fAS  = pr1ᵉ (pr2ᵉ (fibrant-witness WAS))
    ftAS = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WAS)))
    tGm  = pr1ᵉ (fibrant-witness WG)
    fGm  = pr1ᵉ (pr2ᵉ (fibrant-witness WG))
    ftGm = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WG)))
    tfGm = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WG)))

  -- matches of the section spaces
  MT : UU (ℓS ⊔ 𝓤)
  MT = fibrant-match WT
  MAF : UU (ℓS ⊔ 𝓤)
  MAF = fibrant-match WAF
  MAS : UU (ℓS ⊔ 𝓤)
  MAS = fibrant-match WAS
  MG : UU (ℓS ⊔ 𝓤)
  MG = fibrant-match WG

  -- matches of the extension types over a boundary z
  private
    WExt : (z : (φ : Φ) → C (Ai φ)) → isFibrant (Ext i (λ ψ → C (A ψ)) z)
    WExt z = Ext-isFibrant cof A z

  MExt : ((φ : Φ) → C (Ai φ)) → UU (ℓS ⊔ 𝓤)
  MExt z = fibrant-match (WExt z)

  private
    toExt : (z : (φ : Φ) → C (Ai φ))
          → Ext i (λ ψ → C (A ψ)) z → C (MExt z)
    toExt z = pr1ᵉ (fibrant-witness (WExt z))
    fromExt : (z : (φ : Φ) → C (Ai φ))
            → C (MExt z) → Ext i (λ ψ → C (A ψ)) z
    fromExt z = pr1ᵉ (pr2ᵉ (fibrant-witness (WExt z)))
    ftExt : (z : (φ : Φ) → C (Ai φ)) (w : Ext i (λ ψ → C (A ψ)) z)
          → fromExt z (toExt z w) =ᵉ w
    ftExt z = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness (WExt z))))
    tfExt : (z : (φ : Φ) → C (Ai φ)) (x : C (MExt z))
          → toExt z (fromExt z x) =ᵉ x
    tfExt z = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness (WExt z))))

    -- realignment of an extension-type match along a strict equality of
    -- boundaries
    shiftExt : {z z' : (φ : Φ) → C (Ai φ)} (E : z =ᵉ z')
             → C (MExt z) → C (MExt z')
    shiftExt E s = exo-tr (λ w → C (MExt w)) E s

  -- the canonical match of the codomain Σ (t : Π_Φ T). Ext_i(A, f∙t) of Θ
  MΣ : UU (ℓS ⊔ 𝓤)
  MΣ = Σ MT (λ mt → MExt (f∙ (fT (c mt))))

  --------------------------------------------------------------------------
  -- The hand-rolled fibrancy witness of GlueInputTm with match MΣ.
  --------------------------------------------------------------------------

  private
    toΣ' : GlueInputTm → C MΣ
    toΣ' w = c ( ic (tT (pr1ᵉ w))
               , ic (shiftExt (exo-ap f∙ (exo-inv (ftT (pr1ᵉ w))))
                              (toExt (f∙ (pr1ᵉ w)) (pr2ᵉ w))) )

    fromΣ' : C MΣ → GlueInputTm
    fromΣ' s = fT (c (pr1 (ic s)))
             ,ᵉ fromExt (f∙ (fT (c (pr1 (ic s))))) (c (pr2 (ic s)))

    -- round trip on the exo side, by exo-J on the witness equality
    fromExt-tr-lemma : {t₁ t₀ : (φ : Φ) → C (T φ)} (E : t₁ =ᵉ t₀)
        (a : Ext i (λ ψ → C (A ψ)) (f∙ t₀))
      → exo-tr (λ t' → Ext i (λ ψ → C (A ψ)) (f∙ t')) E
          (fromExt (f∙ t₁)
            (shiftExt (exo-ap f∙ (exo-inv E)) (toExt (f∙ t₀) a)))
        =ᵉ a
    fromExt-tr-lemma {t₀ = t₀} reflᵉ a = ftExt (f∙ t₀) a

    ftΣ' : (w : GlueInputTm) → fromΣ' (toΣ' w) =ᵉ w
    ftΣ' (t ,ᵉ a) =
      dep-pair-=ᵉ _ _ (ftT t ,ᵉ fromExt-tr-lemma (ftT t) a)

    -- round trip on the match side: the two witness laws differ by a loop of
    -- strict equalities, which UIPᵉ collapses
    tfΣ' : (s : C MΣ) → toΣ' (fromΣ' s) =ᵉ s
    tfΣ' s =
      exo-concat
        (exo-ap (λ q → c ( ic (tT (fT (c mt)))
                         , ic (shiftExt E₁ q) ))
                (tfExt (f∙ (fT (c mt))) (c me)))
        (pairΣC-eq (tfT (c mt)) W)
      where
      mt = pr1 (ic s)
      me = pr2 (ic s)
      E₁ = exo-ap f∙ (exo-inv (ftT (fT (c mt))))
      E₂ = exo-ap (λ h → f∙ (fT h)) (tfT (c mt))
      W : exo-tr (λ (h : C MT) → C (MExt (f∙ (fT h)))) (tfT (c mt))
            (shiftExt E₁ (c me))
          =ᵉ c me
      W =
        exo-concat (exo-tr-ap' (λ h → f∙ (fT h)) (tfT (c mt)))
        (exo-concat (exo-tr-concat E₁ E₂)
                    (exo-ap-tr (UIPᵉ (exo-concat E₁ E₂) reflᵉ)))

    WΣ' : isFibrant GlueInputTm
    WΣ' = isfibrant MΣ (toΣ' ,ᵉ (fromΣ' ,ᵉ (ftΣ' ,ᵉ tfΣ')))

  --------------------------------------------------------------------------
  -- The three matched maps.
  --------------------------------------------------------------------------

  -- Θ, matched (the rendering of Θ through the witnesses WG and WΣ')
  Θ-hat : MG → MΣ
  Θ-hat mg = ic (toΣ' (Θ (fGm (c mg))))

  -- κ(t, (a₀, w)) = a₀, matched
  κ-hat : MΣ → MAS
  κ-hat w = ic (tAS (pr1ᵉ (fromExt (f∙ (fT (c (pr1 w)))) (c (pr2 w)))))

  -- unglue ⊙ (−), matched
  unglue-match : MG → MAS
  unglue-match mg = ic (tAS (pr1ᵉ (unglue⊙ (fGm (c mg)))))

  -- κ-hat ∘ Θ-hat is unglue-match (strict associativity, read through the
  -- witness laws)
  private
    fromExt-pr1-shift : {z z' : (φ : Φ) → C (Ai φ)} (E : z =ᵉ z')
        (s : C (MExt z))
      → pr1ᵉ (fromExt z' (shiftExt E s)) =ᵉ pr1ᵉ (fromExt z s)
    fromExt-pr1-shift reflᵉ s = reflᵉ

  κΘ~unglue : (mg : MG) → Id (κ-hat (Θ-hat mg)) (unglue-match mg)
  κΘ~unglue mg = cic-eq (exo-ap tAS step)
    where
    b = fGm (c mg)
    E = exo-ap f∙ (exo-inv (ftT (res-p b)))
    step : pr1ᵉ (fromExt (f∙ (fT (tT (res-p b))))
                   (shiftExt E (toExt (f∙ (res-p b)) (unglue⊙ b))))
           =ᵉ pr1ᵉ (unglue⊙ b)
    step =
      exo-concat (fromExt-pr1-shift E (toExt (f∙ (res-p b)) (unglue⊙ b)))
                 (exo-ap pr1ᵉ (ftExt (f∙ (res-p b)) (unglue⊙ b)))

  --------------------------------------------------------------------------
  -- Step B: κ-hat is an equivalence.
  --------------------------------------------------------------------------

  private
    -- the restriction map, matched
    r-hat : MAS → MAF
    r-hat m = ic (tAF (restrict i (fAS (c m))))

    HcR : (h : (ψ : Ψ) → C (A ψ))
        → Id (r-hat (ic (tAS h))) (ic (tAF (restrict i h)))
    HcR h = cic-eq (exo-ap (λ h' → tAF (restrict i h')) (ftAS h))

    module Eng = MatchedFibreEngine (i* i A) WAF WExt WAS r-hat HcR

    -- f∙, matched, is an equivalence: Step A over the cofibrant Φ
    module FA = ProductEquiv cofΦ T Ai
                  (λ φ → pr1 (ic (f φ))) (λ φ → c (pr2 (ic (f φ))))

    f-hat : MT → MAF
    f-hat = FA.v-match

    -- the equivalence chain MΣ ≃ MAS
    eB : MΣ ≃ MAS
    eB = ≃-trans e1 (≃-trans e2 (≃-trans e3 e4))
      where
      e1 : MΣ ≃ Σ MT (λ mt → fiber r-hat (f-hat mt))
      e1 = tot (λ mt → pr1 (Eng.matched-fibre-equiv (f∙ (fT (c mt)))))
         , tot-isEquiv _
             (λ mt → pr2 (Eng.matched-fibre-equiv (f∙ (fT (c mt)))))
      e2 : Σ MT (λ mt → fiber r-hat (f-hat mt))
         ≃ Σ MAS (λ ma → Σ MT (λ mt → Id (r-hat ma) (f-hat mt)))
      e2 = swapΣ
      e3 : Σ MAS (λ ma → Σ MT (λ mt → Id (r-hat ma) (f-hat mt)))
         ≃ Σ MAS (λ ma → fiber f-hat (r-hat ma))
      e3 = tot (λ ma → tot (λ mt → λ q → q ⁻¹))
         , tot-isEquiv _
             (λ ma → tot-isEquiv _ (λ mt → inv-path-isEquiv))
      e4 : Σ MAS (λ ma → fiber f-hat (r-hat ma)) ≃ MAS
      e4 = pr1
         , pr1-contr-isEquiv (λ ma → FA.v-match-isEquiv (r-hat ma))

    eB~κ : (w : MΣ) → Id (pr1 eB w) (κ-hat w)
    eB~κ (mt , me) = cic-eq (exo-ap tAS step)
      where
      z = f∙ (fT (c mt))
      step : pr1ᵉ (fromExt (fAF (tAF z))
                     (shiftExt (exo-inv (ftAF z)) (c me)))
             =ᵉ pr1ᵉ (fromExt z (c me))
      step = fromExt-pr1-shift (exo-inv (ftAF z)) (c me)

  κ-hat-isEquiv : isEquiv κ-hat
  κ-hat-isEquiv = isEquiv-htpy eB~κ (pr2 eB)

  --------------------------------------------------------------------------
  -- Item (3): a strict two-sided inverse of Θ makes unglue ⊙ (−) an
  -- equivalence, no pointwise invertibility of unglue.
  --------------------------------------------------------------------------

  Θ-hat-isEquiv-of-inverse :
      StrictInverse i A T f G p ung ubd → isEquiv Θ-hat
  Θ-hat-isEquiv-of-inverse (Θ⁻¹ ,ᵉ (retr ,ᵉ sect)) =
    pr2 (match-equiv WG WΣ' (Θ ,ᵉ (Θ⁻¹ ,ᵉ (retr ,ᵉ sect))))

  unglue-equiv-of-strict-inverse :
      StrictInverse i A T f G p ung ubd → isEquiv unglue-match
  unglue-equiv-of-strict-inverse S =
    isEquiv-htpy κΘ~unglue
      (∘-is-equiv Θ-hat κ-hat (Θ-hat-isEquiv-of-inverse S) κ-hat-isEquiv)

  --------------------------------------------------------------------------
  -- Item (2): the homotopy form makes Θ an equivalence, and the constructor
  -- package holds up to homotopy with strict term boundary.
  --------------------------------------------------------------------------

  module Package2 (inv : (ψ : Ψ) → C (isEquiv (ung ψ))) where

    private
      module UA = ProductEquiv cofΨ G A ung inv

    -- Step A over the cofibrant Ψ: the matched unglue ⊙ (−) is an equivalence
    unglue-match-isEquiv : isEquiv unglue-match
    unglue-match-isEquiv = UA.v-match-isEquiv

    -- Step C: Θ-hat is an equivalence (2-out-of-3).
    -- contractibility centres taken below (b₀m, γ, and the contraction path
    -- in glue-linked-η) stay neutral during conversion checking; a
    -- transparent witness makes those whnf's normalise the whole Step A-C
    -- equivalence chain (observed: > 25 min / > 14 GB).  The witness is a
    -- proof of a proposition; nothing needs it to unfold.
    abstract
      Θ-hat-isEquiv : isEquiv Θ-hat
      Θ-hat-isEquiv =
        isEquiv-left-cancel Θ-hat κ-hat κ-hat-isEquiv
          (isEquiv-htpy (λ mg → (κΘ~unglue mg) ⁻¹) unglue-match-isEquiv)

    -- contractible uniqueness: the homotopy fibre of Θ-hat over any matched
    -- input (the pair of a glue term and its linked β-path) is contractible
    glue-unique : (w : MΣ) → is-contr (fiber Θ-hat w)
    glue-unique = Θ-hat-isEquiv

    ------------------------------------------------------------------------
    -- The glue construction: for an input (t, a), a section glue(t,a) with
    -- strict term boundary and a linked β-path Θ-hat ⌜glue(t,a)⌝ = ⌜(t,a)⌝.
    ------------------------------------------------------------------------

    module GlueTerm (t : (φ : Φ) → C (T φ))
                    (a : Ext i (λ ψ → C (A ψ)) (f∙ t)) where

      -- the matched input point
      ⌜ta⌝ : MΣ
      ⌜ta⌝ = ic (toΣ' (t ,ᵉ a))

      private
        fib-c : is-contr (fiber Θ-hat ⌜ta⌝)
        fib-c = Θ-hat-isEquiv ⌜ta⌝

      -- the homotopy inverse image and its path
      b₀m : MG
      b₀m = pr1 (pr1 fib-c)

      γ : Id (Θ-hat b₀m) ⌜ta⌝
      γ = pr2 (pr1 fib-c)

      private
        b₀ : (ψ : Ψ) → C (G ψ)
        b₀ = fGm (c b₀m)

        -- the first-component path of γ, converted to pointwise paths
        p1γ : Id (ic (tT (res-p b₀))) (ic (tT t))
        p1γ = ap pr1 γ

        WIdT = Π-fibrant-witness
                 (cofΦ (λ φ → Id (ic (res-p b₀ φ))
                                 (ic (fT (c (ic (tT t))) φ))))

        q̃ : fibrant-match WIdT
        q̃ = pr1 (funext-Id-equiv cofΦ T (res-p b₀) (ic (tT t))) p1γ

        r₀ : (φ : Φ) → C (Id (ic (res-p b₀ φ)) (ic (fT (tT t) φ)))
        r₀ = pr1ᵉ (pr2ᵉ (fibrant-witness WIdT)) (c q̃)

        r' : (φ : Φ) → Id (ic (res-p b₀ φ)) (ic (t φ))
        r' φ = ic (r₀ φ) · cic-eq (happlyᵉ (ftT t) φ)

        -- the boundary datum in G, and the weak agreement with b₀
        tbd : (φ : Φ) → C (G (i φ))
        tbd = exo-tr (λ H → (ξ : Φ) → C (H ξ)) (exo-inv p) t

        e' : (φ : Φ) → Id (ic (tbd φ)) (ic (b₀ (i φ)))
        e' φ = tG-path-convert i G T p b₀ t r' φ

        -- RS 4.10 (homotopy extension property), through the packaged opaque
        -- export of Extension.RS410Pack: the strict extension and its
        -- homotopy agreement are produced by one application `hep`, so the
        -- conversion relating them is performed once at the generic level
        -- and instances never unfold the RS46 contractibility engine at the
        -- large argument terms (b₀ is the centre of a contractibility proof;
        -- transparent `a'`/`a'-agrees-b` here blew up: > 14 min / > 5 GB).
        pack : HEP cof triv G b₀ tbd e'
        pack = hep cof triv G b₀ tbd e'

        aext : Ext i (λ ψ → C (G ψ)) tbd
        aext = pr1ᵉ pack

      -- the glue term ...
      glue-tm : (ψ : Ψ) → C (G ψ)
      glue-tm = pr1ᵉ aext

      -- ... with strict term boundary (item (5), rule Term-Bdry) ...
      glue-strict-bdry : res-p glue-tm =ᵉ t
      glue-strict-bdry =
        exo-concat
          (exo-ap (exo-tr (λ H → (ξ : Φ) → C (H ξ)) p) (pr2ᵉ aext))
          (tr-inv-tr (λ H → (ξ : Φ) → C (H ξ)) p t)

      private
        glue-agrees-b₀ : (ψ : Ψ) → Id (ic (glue-tm ψ)) (ic (b₀ ψ))
        glue-agrees-b₀ ψ = ic (pr2ᵉ pack ψ)

      -- ... and the path from its match to the homotopy inverse image
      glue-b₀m-path : Id (ic (tGm glue-tm)) b₀m
      glue-b₀m-path =
        MatchPath.match-path-of-pointwise cofΨ G glue-tm b₀ glue-agrees-b₀
        · cic-eq (tfGm (c b₀m))

      -- the linked β-path: Θ-hat ⌜glue(t,a)⌝ = ⌜(t,a)⌝
      glue-linked-β : Id (Θ-hat (ic (tGm glue-tm))) ⌜ta⌝
      glue-linked-β = ap Θ-hat glue-b₀m-path · γ

    -- the linked η-path: for a section b, glue(Θ b) = b (in the match)
    glue-linked-η : (b : (ψ : Ψ) → C (G ψ))
      → Id (ic (tGm (GlueTerm.glue-tm (res-p b) (unglue⊙ b))))
           (ic (tGm b))
    glue-linked-η b =
      GlueTerm.glue-b₀m-path (res-p b) (unglue⊙ b)
      · (ap pr1 (pr2 (Θ-hat-isEquiv (ic (toΣ' (Θ b)))) (ic (tGm b) , χ))) ⁻¹
      where
      χ : Id (Θ-hat (ic (tGm b))) (ic (toΣ' (Θ b)))
      χ = cic-eq (exo-ap (λ h → toΣ' (Θ h)) (ftGm b))

    ------------------------------------------------------------------------
    -- Item (2), packaged as stated in the paper.
    ------------------------------------------------------------------------

    record HomotopyConstructorPackage : UUᵉ (ℓS ⊔ 𝓤) where
      field
        Θ-is-equiv : C (isEquiv Θ-hat)
        glue : (t : (φ : Φ) → C (T φ))
          (a : Ext i (λ ψ → C (A ψ)) (f∙ t)) →
          (ψ : Ψ) → C (G ψ)
        glue-strict-boundary :
          (t : (φ : Φ) → C (T φ))
          (a : Ext i (λ ψ → C (A ψ)) (f∙ t)) →
          res-p (glue t a) =ᵉ t
        linked-β :
          (t : (φ : Φ) → C (T φ))
          (a : Ext i (λ ψ → C (A ψ)) (f∙ t)) →
          C (Id (Θ-hat (ic (tGm (glue t a))))
                (ic (toΣ' (t ,ᵉ a))))
        linked-η : (b : (ψ : Ψ) → C (G ψ)) →
          C (Id (ic (tGm (glue (res-p b) (unglue⊙ b))))
                (ic (tGm b)))
        contractible-unique : (w : C MΣ) →
          C (is-contr (fiber Θ-hat (ic w)))

    homotopy-constructor-package : HomotopyConstructorPackage
    homotopy-constructor-package = record
      { Θ-is-equiv = c Θ-hat-isEquiv
      ; glue = GlueTerm.glue-tm
      ; glue-strict-boundary = GlueTerm.glue-strict-bdry
      ; linked-β = λ t a → c (GlueTerm.glue-linked-β t a)
      ; linked-η = λ b → c (glue-linked-η b)
      ; contractible-unique = λ w → c (glue-unique (ic w))
      }

{- References:

  [RS]         Emily Riehl and Michael Shulman.  A type theory for synthetic
               ∞-categories.  Higher Structures 1(1):147-224, 2017.
               doi:10.21136/hs.2017.06

-}