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

----------------------------------------------------------------------------------------------------
--   Agda auto-formalization of the paper
--
--         Extension Types for Free
--             Nicolai Kraus
--
--
-- This is an auto-formalization, written by Claude Opus 4.8 and Opus 5.0. The input was the
-- (human-written) paper. I (Nicolai Kraus) made many requests to change structure and namings,
-- wrote comments, but made only minor manual edits to the Agda code itself. I manually checked
-- that the formalized statements are readable and coincide with the paper statements.
--
-- This file provides an interface between the paper and the Agda auto-formalization. It lists all
-- statements of the paper in order. If a statement is internal to 2LTT, it is formalized, and the
-- formalization is given. This is the case for everything before the Conclusions section, i.e.
-- Sections 2-5. The conclusions section discusses type theories rather than results inside a single
-- type theory, and this is not formalizable in 2LTT. The statements in the conclusions (6.1, 6.2,
-- 6.3) are thus only given as comments below, without formalized proofs. The statements requiring
-- outer pushouts (Lemma 3.5, Lemma 3.8), axiomatic inputs in the paper as well ("assumed when they
-- exist"), are formalized with a condition, namely the assumed exo-pushout with strict UMP
-- (`Extension.ExoPushout`).
----------------------------------------------------------------------------------------------------

module index where

-- The following module imports the entire development.
import Extension.Everything

-- The development builds on Elif Uskuplu's 2LTT formalization.
-- Uskuplu's paper DOI:         https://doi.org/10.1017/S0960129525100297
-- Uskuplu's Agda repository:   https://github.com/ElifUskuplu/2LTT-Agda
-- Version used:                commit b0640910fae9263fe9031636923460dc124920f3
--                              of 6 August 2025 ("minor edits to make the library
--                              compatible with Agda 2.8"), the (at the time of writing)
--                              head of the master branch.  The non-cumulativity variant
--                              `2LTT_C` is the one imported.
-- The following module bundles the used parts:
open import Extension.Prelude

-- own imports:
import Extension.Univalence              as Univalence
import Extension.Core                    as Core
import Extension.RS                      as RS
import Extension.RSHomotopy              as RSHomotopy
import Extension.CofibFibration          as CofibFibration
import Extension.RS46                    as RS46
import Extension.RS410                   as RS410
import Extension.RS48                    as RS48
import Extension.RS412                   as RS412
import Extension.FundamentalId           as FundamentalId
import Extension.PiTruncation            as PiTruncation
import Extension.SigmaTruncation         as SigmaTruncation
import Extension.RS412Ext                as RS412Ext
import Extension.ExtFamIso               as ExtFamIso
import Extension.RS48Ext                 as RS48Ext
import Extension.RelFunext               as RelFunext
import Extension.WeakStrict              as WeakStrict
import Extension.Instances               as Instances
import Extension.Fibre                   as Fibre
import Extension.CanonicalFibre          as CanonicalFibre
import Extension.HomFillers              as HomFillers
import Extension.Glue                    as Glue
import Extension.GlueStructure           as GlueStructure
import Extension.GlueRules               as GlueRules
import Extension.GlueUA                  as GlueUA
import Extension.UAFromSection           as UAFromSection
import Extension.WeakGlueUA              as WeakGlueUA
import Extension.WeakGlueUAFibrant       as WeakGlueUAFibrant
import Extension.UAStrongGlue            as UAStrongGlue
import Extension.GlueStrengthChain3      as GlueStrengthChain3
import Extension.GlueDataFibrant         as GlueDataFibrant
import Extension.GlueSandwich            as GlueSandwich
import Extension.GlueSandwichFibrant     as GlueSandwichFibrant
import Extension.CoercionLaws            as CoercionLaws
import Extension.GlueSandwichComplete    as GlueSandwichComplete
import Extension.GlueSandwichGeneral     as GlueSandwichGeneral
import Extension.Conservativity          as Conservativity
import Extension.TheoryComparison        as TheoryComparison
import Extension.CofibClosure            as CofibClosure
import Extension.PropRealign             as PropRealign
import Extension.RS411                   as RS411
import Extension.RS410Pack               as RS410Pack
import Extension.TriangleStrictification as TriangleStrictification
import Extension.GlueLiteralRules        as GlueLiteralRules
import Extension.GlueHomotopySemantic    as GlueHomotopySemantic
import Extension.GlueSandwichFull        as GlueSandwichFull
import Extension.CoercionLawsNamed       as CoercionLawsNamed
import Extension.ExoPushout              as ExoPushout
import Extension.RS42                    as RS42
import Extension.RS45                    as RS45
import Extension.CanonicalFillers        as CanonicalFillers
import Extension.GlueConstructorPackage  as GlueConstructorPackage
import Extension.Corollary55             as Corollary55

private
  variable
    ℓΦ ℓΨ ℓA : Level

---------------------------------------------------------------------------------------------
{- §2  Two-level type theory as a framework for Extension Types
(the results below are in §2.2, Strictifications) -}
---------------------------------------------------------------------------------------------

-- Lemma 2.2. The strict and the homotopy fibre of a fibration over a fibrant
-- base are equivalent, by the canonical map (y, q) ↦ (y, ι q).
-- `Lemma-2-2-strict` is that statement, with the homotopy fibre read through
-- fibrant matches.  Since the lemma also says which map the equivalence is,
-- `Lemma-2-2-map` and `Lemma-2-2-equiv` give the map and its invertibility
-- separately; `Lemma-2-2-strict` is the pair of the two.  The two family
-- entries below compute both fibres of an evaluation to P x₀; they are in two
-- halves because an inner equivalence cannot relate the strict fibre, an exo
-- type, to anything directly.
Lemma-2-2-strict
  : {ℓ : Level} {E F : UUᵉ ℓ} (WF : isFibrant F) (g : E → F)
    (fibW : (p : F) → isFibrant (Glue.fibᵉ g p)) (p₀ : F) →
    CanonicalFibre.fibre-match WF g fibW p₀
    ≃ fiber (λ r → pr1 r) (ic (CanonicalFibre.to-match WF g fibW p₀))
Lemma-2-2-strict = CanonicalFibre.canonical-fibre-equiv

Lemma-2-2-map
  : {ℓ : Level} {E F : UUᵉ ℓ} (WF : isFibrant F) (g : E → F)
    (fibW : (p : F) → isFibrant (Glue.fibᵉ g p)) (p₀ : F) →
    CanonicalFibre.fibre-match WF g fibW p₀
    → fiber (λ r → pr1 r) (ic (CanonicalFibre.to-match WF g fibW p₀))
Lemma-2-2-map = CanonicalFibre.canonical-map
Lemma-2-2-equiv
  : {ℓ : Level} {E F : UUᵉ ℓ} (WF : isFibrant F) (g : E → F)
    (fibW : (p : F) → isFibrant (Glue.fibᵉ g p)) (p₀ : F) →
    isEquiv (Lemma-2-2-map WF g fibW p₀)
Lemma-2-2-equiv = CanonicalFibre.canonical-map-isEquiv

Lemma-2-2-family-strict
  : {ℓX ℓ : Level} {X : UU ℓX} (P : X → UU ℓ) (x₀ : X) → Fibre.Sfibreᶜ P x₀ ≅ C (P x₀)
Lemma-2-2-family-strict = Fibre.strict-fibre-match
Lemma-2-2-family-homotopy
  : {ℓX ℓ : Level} {X : UU ℓX} (P : X → UU ℓ) (x₀ : X) → Fibre.Hfibre P x₀ ≃ P x₀
Lemma-2-2-family-homotopy = Fibre.homotopy-fibre-equiv

Lemma-2-2-ext-instance
  : {ℓ : Level} {ℓS : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ) (p₀ : Πᵉ Φ (λ b → C (Y (i b)))) →
    CanonicalFibre.fibre-match (Π-fibrant-witness (cofΦ (λ φ → Y (i φ))))
      (CofibFibration.i* i Y) (CofibFibration.Ext-isFibrant cof Y) p₀
    ≃ fiber (λ r → pr1 r)
        (ic
          (CanonicalFibre.to-match (Π-fibrant-witness (cofΦ (λ φ → Y (i φ))))
            (CofibFibration.i* i Y) (CofibFibration.Ext-isFibrant cof Y) p₀))
Lemma-2-2-ext-instance = CanonicalFibre.strict-to-homotopy-ext

-- Lemma 2.3. Assume a strictly commuting square with i the left and f the right
-- vertical morphism. Here, i : A ↪ B is a cofibration, A cofibrant, and f : Y ↠ X
-- a fibration with X fibrant. As in Lemma 2.2, we set Y = Σ X Z for some family Z and
-- f = pr₁.  Cofibrancy of B is derived by `CofibClosure.cofib-codomain-cofibrant`. The strict fillers
--     D  = Σᵉ (h : B → C Y). (h ∘ i =ᵉ l) ×ᵉ (f ∘ h =ᵉ k)
-- and the coherent homotopy fillers
--     D′ = Σ (h : ⟨B → Y⟩). Σ (p₁ : h∘i = ⌜l⌝). Σ (p₂ : f∘h = ⌜k⌝). (ap p₁)⁻¹ · ap p₂ = ι e₀
-- are both fibrant, and the canonical map D → D′ is an equivalence.
Lemma-2-3
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    fibrant-match (HomFillers.D-isFibrant cof2 cofA X Z l k e₀)
    ≃ HomFillers.D′ cof2 cofA X Z l k e₀
Lemma-2-3             = CanonicalFillers.canonical-fillers
Lemma-2-3-map
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    fibrant-match (HomFillers.D-isFibrant cof2 cofA X Z l k e₀) →
    HomFillers.D′ cof2 cofA X Z l k e₀
Lemma-2-3-map         = CanonicalFillers.canonical-fill
Lemma-2-3-equiv
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    isEquiv (Lemma-2-3-map cof2 cofA X Z l k e₀)
Lemma-2-3-equiv       = CanonicalFillers.canonical-fillers-equiv
Lemma-2-3-existence
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    fibrant-match (HomFillers.D-isFibrant cof2 cofA X Z l k e₀)
    ≃ HomFillers.D′ cof2 cofA X Z l k e₀
Lemma-2-3-existence   = HomFillers.hom-fillers-equiv
Lemma-2-3-D-fibrant
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    isFibrant (HomFillers.D cof2 cofA X Z l k e₀)
Lemma-2-3-D-fibrant   = HomFillers.D-isFibrant
Lemma-2-3-D'
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    UU (ℓS ⊔ ℓ)
Lemma-2-3-D'          = HomFillers.D′
Lemma-2-3-h-canonical
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B} (cof2 : RelFunext.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))) →
    fibrant-match (Π-fibrant-witness (HomFillers.cofB cof2 cofA X Z l k e₀ (λ _ → Σ X Z)))
    ≃ HomFillers.ΣB cof2 cofA X Z l k e₀
Lemma-2-3-h-canonical = HomFillers.h-match-canonical

-- Lemma 2.4. For a fixed partial section l, the strict extension type is
-- fibrant and its canonical match is equivalent to the homotopy fibre of the
-- matched restriction map over l. This is the comparison between
-- strict and homotopy extensions for a dependent fibrant family. The later
-- section-splitting aliases record the totalised form as additional machinery.
Lemma-2-4
  : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (cofA : isCofibrant A ℓ)
    (Y : B → UU ℓ) (l : (a : A) → C (Y (i a))) →
    CanonicalFibre.fibre-match
      (Π-fibrant-witness (cofA (λ a → Y (i a))))
      (CofibFibration.i* i Y) (CofibFibration.Ext-isFibrant (pr1ᵉ c2) Y) l
    ≃ fiber (λ r → pr1 r)
        (ic (CanonicalFibre.to-match
          (Π-fibrant-witness (cofA (λ a → Y (i a))))
          (CofibFibration.i* i Y) (CofibFibration.Ext-isFibrant (pr1ᵉ c2) Y) l))
Lemma-2-4 c2 = CanonicalFibre.strict-to-homotopy-ext (pr1ᵉ c2)

Lemma-2-4-section-splitting
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ) →
    fibrant-match (Π-fibrant-witness (cofΨ Y))
    ≃ fibrant-match
        (isFibrant-Σ (Π-fibrant-witness (cofΦ (λ φ → Y (i φ))))
          (CofibFibration.Ext-isFibrant cof Y))
Lemma-2-4-section-splitting = WeakStrict.weak=strict
Lemma-2-4-dep
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ) →
    fibrant-match (Π-fibrant-witness (cofΨ Y))
    ≃ fibrant-match
        (isFibrant-Σ (Π-fibrant-witness (cofΦ (λ φ → Y (i φ))))
          (CofibFibration.Ext-isFibrant cof Y))
Lemma-2-4-dep = WeakStrict.weak=strict

-- Lemma 3.14: a weak (homotopy) boundary agreement can be strictified. The
-- constructive proof is the homotopy extension property, Lemma 3.14 below.
Lemma-3-14-strictify
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ))
    (a : (φ : Φ) → C (Y (i φ))) (e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ)))) →
    Core.Ext i (λ ψ → C (Y ψ)) a
Lemma-3-14-strictify c2 = RS410.a' (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-strictify-agrees
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ))
    (a : (φ : Φ) → C (Y (i φ))) (e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ)))) (ψ : Ψ) →
    Id (ic (Core.ext-app (Lemma-3-14-strictify c2 Y b a e) ψ)) (ic (b ψ))
Lemma-3-14-strictify-agrees c2 = RS410.a'-agrees-b (pr1ᵉ c2) (pr2ᵉ c2)

-- The constant-family instance of Lemma 3.14 gives triangle
-- strictification: h agrees with f strictly on Φ, the homotopy from h to g
-- restricts strictly to the given homotopy H, after the explicit transport
-- forced by propositional strict equality.
Lemma-3-14-triangle-h
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : UU ℓ) (f : Φ → C Y) (g : Ψ → C Y)
    (H : (φ : Φ) → Id (ic (f φ)) (ic (g (i φ)))) →
    Ψ → C Y
Lemma-3-14-triangle-h c2 = TriangleStrictification.h (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-triangle-top-strict
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : UU ℓ) (f : Φ → C Y) (g : Ψ → C Y)
    (H : (φ : Φ) → Id (ic (f φ)) (ic (g (i φ)))) →
    (λ φ → Lemma-3-14-triangle-h c2 Y f g H (i φ)) =ᵉ f
Lemma-3-14-triangle-top-strict c2 = TriangleStrictification.top-strict (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-triangle-globe
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : UU ℓ) (f : Φ → C Y) (g : Ψ → C Y)
    (H : (φ : Φ) → Id (ic (f φ)) (ic (g (i φ)))) (ψ : Ψ) →
    Id (ic (Lemma-3-14-triangle-h c2 Y f g H ψ)) (ic (g ψ))
Lemma-3-14-triangle-globe c2 = TriangleStrictification.G (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-triangle-globe-strict
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : UU ℓ) (f : Φ → C Y) (g : Ψ → C Y)
    (H : (φ : Φ) → Id (ic (f φ)) (ic (g (i φ)))) →
    (λ φ → c (Lemma-3-14-triangle-globe c2 Y f g H (i φ)))
    =ᵉ (λ φ → exo-tr (λ v → C (Id (ic v) (ic (g (i φ)))))
          (exo-inv (happlyᵉ (Lemma-3-14-triangle-top-strict c2 Y f g H) φ))
          (c (H φ)))
Lemma-3-14-triangle-globe-strict c2 =
  TriangleStrictification.globe-restricts-strictly (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-triangle-no-strict-globe
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : UU ℓ) (f : Φ → C Y) (g : Ψ → C Y) →
    ((φ : Φ) → Id (ic (f φ)) (ic (g (i φ)))) →
    (h' : Ψ → C Y) →
    (λ φ → h' (i φ)) =ᵉ f →
    h' =ᵉ g →
    (λ φ → g (i φ)) =ᵉ f
Lemma-3-14-triangle-no-strict-globe c2 =
  TriangleStrictification.no-strict-globe (pr1ᵉ c2) (pr2ᵉ c2)


----------------------------------------------------------------------------------------------------
{- §3  The Riehl–Shulman extension-type calculus -}
----------------------------------------------------------------------------------------------------


-- Definition 3.9: the predicate "(i, Y) satisfies relative function
-- extensionality" (Rzk's WeakExtExt / RS Axiom 4.6), which is the trivial-fibration half
-- of the 2LTT cofibration property, read through [2LTT, Lem 3.18].
Definition-3-9
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ) →
    UUᵉ ((ℓΦ ⊔ ℓΨ) ⊔ lsuc ℓ)
Definition-3-9 = RelFunext.satisfies-rel-funext

-- Remark 3.10: a reading of Definition 3.9 and
-- Lemma 3.11 (relative funext = funext for the shape-indexed product; RS must postulate it
-- because their cofibrations lack the trivial-fibration half).  Discussion only; the
-- mathematical content is the pair Definition-3-9 / Lemma-3-11.

-- Lemma 3.11: relative funext holds for every full 2LTT cofibration,
-- with no cofibrancy of Φ or Ψ, RS's axiom is a theorem in this framework.  In the
-- Lem 3.18 packaging the trivial half is the statement, so the lemma is the projection;
-- the content lives in the instance: cofibrant shapes discharge the trivial half from the
-- fibration half alone (`Lemma-3-11-cofibrant`, the argument of Extension.RS46).
Lemma-3-11
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ) →
    Definition-3-9 (pr1ᵉ c2)
Lemma-3-11           = RelFunext.rel-funext-holds-2LTT
Lemma-3-11-cofibrant
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ) →
    isCofibrant Ψ ℓ → isCofibrant Φ ℓ → Definition-3-9 cof
Lemma-3-11-cofibrant = RelFunext.rel-funext-holds

-- Corollary 3.12, strict realignment of propositional components.  Rendering: the paper's
-- type of realignments  Realign = Σᵉ (s' : Πψ.Sψ). (π₁∘s' =ᵉ π₁∘s) ×ᵉ (s'∘i =ᵉ s₀)  is an exo
-- type; it is strictly isomorphic to Extᵢ(P', l) for the property family along the data of s
-- (`Corollary-3-12-iso`), hence fibrant (`Corollary-3-12-fibrant`), and "contractible" is read
-- through the fibrant match: `Corollary-3-12` states is-contr of the match.  Hypothesis: the
-- full is-cofib-2LTT, the proof is the trivial-fibration half (relative funext) on the
-- inhabited-proposition family; no cofibrancy of Φ or Ψ.  Existence and uniqueness-up-to-
-- homotopy of a realignment are extracted as separate names.
Corollary-3-12
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (D : Ψ → UU ℓ) (P : (ψ : Ψ) → D ψ → UU ℓ) (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
    (s : (ψ : Ψ) → C (PropRealign.S c2 D P propP ψ))
    (s₀ : (φ : Φ) → C (PropRealign.S c2 D P propP (i φ)))
    (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ)))) →
    is-contr (fibrant-match (PropRealign.Realign-isFibrant c2 D P propP s s₀ agr))
Corollary-3-12         = PropRealign.realign-contr
Corollary-3-12-iso
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (D : Ψ → UU ℓ) (P : (ψ : Ψ) → D ψ → UU ℓ) (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
    (s : (ψ : Ψ) → C (PropRealign.S c2 D P propP ψ))
    (s₀ : (φ : Φ) → C (PropRealign.S c2 D P propP (i φ)))
    (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ)))) →
    PropRealign.Realign c2 D P propP s s₀ agr
    ≅ Core.Ext i (λ ψ → C (PropRealign.P' c2 D P propP s s₀ agr ψ))
        (PropRealign.l c2 D P propP s s₀ agr)
Corollary-3-12-iso     = PropRealign.realign-iso
Corollary-3-12-fibrant
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (D : Ψ → UU ℓ) (P : (ψ : Ψ) → D ψ → UU ℓ) (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
    (s : (ψ : Ψ) → C (PropRealign.S c2 D P propP ψ))
    (s₀ : (φ : Φ) → C (PropRealign.S c2 D P propP (i φ)))
    (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ)))) →
    isFibrant (PropRealign.Realign c2 D P propP s s₀ agr)
Corollary-3-12-fibrant = PropRealign.Realign-isFibrant
Corollary-3-12-exists
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (D : Ψ → UU ℓ) (P : (ψ : Ψ) → D ψ → UU ℓ) (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
    (s : (ψ : Ψ) → C (PropRealign.S c2 D P propP ψ))
    (s₀ : (φ : Φ) → C (PropRealign.S c2 D P propP (i φ)))
    (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ)))) →
    PropRealign.Realign c2 D P propP s s₀ agr
Corollary-3-12-exists  = PropRealign.realignment
Corollary-3-12-unique
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (D : Ψ → UU ℓ) (P : (ψ : Ψ) → D ψ → UU ℓ) (propP : (ψ : Ψ) (d : D ψ) → is-prop (P ψ d))
    (s : (ψ : Ψ) → C (PropRealign.S c2 D P propP ψ))
    (s₀ : (φ : Φ) → C (PropRealign.S c2 D P propP (i φ)))
    (agr : (φ : Φ) → c (pr1 (ic (s (i φ)))) =ᵉ c (pr1 (ic (s₀ φ))))
    (r₁ r₂ : PropRealign.Realign c2 D P propP s s₀ agr) →
    Id (ic (pr1ᵉ (fibrant-witness (Corollary-3-12-fibrant c2 D P propP s s₀ agr)) r₁))
      (ic (pr1ᵉ (fibrant-witness (Corollary-3-12-fibrant c2 D P propP s s₀ agr)) r₂))
Corollary-3-12-unique  = PropRealign.realign-unique


-- Definition 3.1: The extension type, as the strict fibre of the restriction map
--     Extᵢ(A , a)  ≔  Σᵉ (f : (ψ : Ψ) → A ψ) . (f ∘ i =ᵉ a).
-- (In the paper, the definition and its displayed formula are one environment, the
-- definition contains the display, sitting in the section intro that fixes the shape
-- inclusion.)
Definition-3-1 : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ}
              → (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA) (a : (φ : Φ) → A (i φ))
              → UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓA)
Definition-3-1 = Core.Ext

-- Lemma 3.2: the RS rules (RS Fig. 4) hold, with strict boundary rule, and with β
-- and η holding definitionally (both proofs are reflᵉ).
Lemma-3-2-intro
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} → Core.ExtensionRules i A a
Lemma-3-2-intro = Core.extension-rules
Lemma-3-2-eval
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} →
    Core.Ext i A a → (ψ : Ψ) → A ψ
Lemma-3-2-eval  = Core.ext-app
Lemma-3-2-bdry
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} (f : Core.Ext i A a) (φ : Φ) →
    Lemma-3-2-eval f (i φ) =ᵉ a φ
Lemma-3-2-bdry  = Core.ext-bdry
Lemma-3-2-β
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} (b : (ψ : Ψ) → A ψ) (p : Core.restrict i b =ᵉ a) (ψ : Ψ) →
    Core.ext-app (Core.ext-λ b p) ψ =ᵉ b ψ
Lemma-3-2-β     = Core.ext-β
Lemma-3-2-η
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} (f : Core.Ext i A a) →
    f =ᵉ Core.ext-λ (Core.ext-app f) (pr2ᵉ f)
Lemma-3-2-η     = Core.ext-η

-- Remark 3.3: the proposition-indexed calculus { A ∣ φ ▷ u } (Zhang; Sterling's
-- "extent"; controlled unfolding) is the instance Ext_{φ→1}, with its intro/elim/boundary rules;
-- and it agrees with the direct Σ-formula.
Remark-3-3-type
  : {ℓφ ℓA : Level} (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) → Instances.PropExtCalculus φ A u
Remark-3-3-type = Instances.prop-ext-calculus
Remark-3-3-intro
  : {ℓφ ℓA : Level} (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) (v : A) →
    ((p : φ) → v =ᵉ u p) → Instances.PropExt-direct φ A u
Remark-3-3-intro  = Instances.inS
Remark-3-3-elim
  : {ℓφ ℓA : Level} (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) → Instances.PropExt-direct φ A u → A
Remark-3-3-elim   = Instances.outS
Remark-3-3-bdry
  : {ℓφ ℓA : Level} (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) (w : Instances.PropExt-direct φ A u)
    (p : φ) →
    Remark-3-3-elim φ A u w =ᵉ u p
Remark-3-3-bdry   = Instances.bdryP
Remark-3-3-direct
  : {ℓφ ℓA : Level} (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (u : φ → A) →
    Instances.PropExt φ A u ≅ Instances.PropExt-direct φ A u
Remark-3-3-direct = Instances.PropExt≅direct

-- Remark 3.3, fibrewise: an extension type along any i is a Π over the codomain of extension
-- types along maps into 1. Over ψ the index is the strict fibre of i and the partial element is
-- the boundary datum transported into it. That index is a strict proposition exactly when i is
-- injective, which being a cofibration does not give.
Remark-3-3-fibrewise
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (A : Ψ → UUᵉ ℓA)
    (a : (φ : Φ) → A (i φ)) →
    Core.Ext i A a ≅ ((ψ : Ψ) → Instances.PropExt-direct
                                  (Instances.im i ψ) (A ψ) (Instances.im-bdry i A a ψ))
Remark-3-3-fibrewise = Instances.fibrewise-decomposition
Remark-3-3-fibrewise-index
  : {ℓΦ ℓΨ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) →
    ((φ φ' : Φ) → i φ =ᵉ i φ' → φ =ᵉ φ') →
    (ψ : Ψ) (z z' : Instances.im i ψ) → z =ᵉ z'
Remark-3-3-fibrewise-index = Instances.im-is-prop

-- Lemma 3.4: currying,  Extᵢ over a Π-family  ≅  Π of extension types.
Lemma-3-4
  : {ℓΦ ℓΨ ℓX ℓY : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (X : UUᵉ ℓX)
    (Y : Ψ → X → UUᵉ ℓY) (f : (φ : Φ) (x : X) → Y (i φ) x) →
    Core.Ext i (λ ψ → (x : X) → Y ψ x) f ≅ ((x : X) → Core.Ext i (λ ψ → Y ψ x) (λ φ → f φ x))
Lemma-3-4 = RS.RS41

-- Lemma 3.5: currying / pushout-product.  Conditionally formalized: outer pushouts
-- do not exist in plain 2LTT, so the pushout P = Φ×ᵉΨ' ∪_{Φ×ᵉΦ'} Ψ×ᵉΦ' is a parameter, an
-- assumed strict cocone with strict UMP (`interface-exo-pushout` below), the paper's
-- hypothesis ("provided this pushout exists in the outer level").  Both isos and their
-- composite, for a general exo family (the paper's fibrant statement is the instance C ∘ A₀);
-- the propositional β-rules of the assumed pushout replace the judgmental ones an actual
-- pushout would have (all coherence discharged by UIPᵉ).
Lemma-3-5
  : {ℓΦ ℓΨ ℓΦ' ℓΨ' ℓP : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Φ' : UUᵉ ℓΦ'} {Ψ' : UUᵉ ℓΨ'}
    (i : Φ → Ψ) (i' : Φ' → Ψ') {P : UUᵉ ℓP} (inlᴾ : Φ ×ᵉ Ψ' → P) (inrᴾ : Ψ ×ᵉ Φ' → P)
    (glueᴾ : (w : Φ ×ᵉ Φ') → inlᴾ (RS42.pp-left i i' w) =ᵉ inrᴾ (RS42.pp-right i i' w))
    (po : {ℓE : Level} →
      ExoPushout.is-exo-pushout (RS42.pp-left i i') (RS42.pp-right i i') inlᴾ inrᴾ glueᴾ ℓE)
    {ℓA : Level} (A : Ψ ×ᵉ Ψ' → UUᵉ ℓA) (cᴾ : (p : P) → A (RS42.i□i' i i' inlᴾ inrᴾ glueᴾ po p)) →
    Core.Ext i (RS42.E₁ i i' inlᴾ inrᴾ glueᴾ po A cᴾ) (RS42.c₁ i i' inlᴾ inrᴾ glueᴾ po A cᴾ)
    ≅ Core.Ext i' (RS42.E₂ i i' inlᴾ inrᴾ glueᴾ po A cᴾ) (RS42.c₂ i i' inlᴾ inrᴾ glueᴾ po A cᴾ)
Lemma-3-5   = RS42.RS42
Lemma-3-5-a
  : {ℓΦ ℓΨ ℓΦ' ℓΨ' ℓP : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Φ' : UUᵉ ℓΦ'} {Ψ' : UUᵉ ℓΨ'}
    (i : Φ → Ψ) (i' : Φ' → Ψ') {P : UUᵉ ℓP} (inlᴾ : Φ ×ᵉ Ψ' → P) (inrᴾ : Ψ ×ᵉ Φ' → P)
    (glueᴾ : (w : Φ ×ᵉ Φ') → inlᴾ (RS42.pp-left i i' w) =ᵉ inrᴾ (RS42.pp-right i i' w))
    (po : {ℓE : Level} →
      ExoPushout.is-exo-pushout (RS42.pp-left i i') (RS42.pp-right i i') inlᴾ inrᴾ glueᴾ ℓE)
    {ℓA : Level} (A : Ψ ×ᵉ Ψ' → UUᵉ ℓA) (cᴾ : (p : P) → A (RS42.i□i' i i' inlᴾ inrᴾ glueᴾ po p)) →
    Core.Ext i (RS42.E₁ i i' inlᴾ inrᴾ glueᴾ po A cᴾ) (RS42.c₁ i i' inlᴾ inrᴾ glueᴾ po A cᴾ)
    ≅ Core.Ext (RS42.i□i' i i' inlᴾ inrᴾ glueᴾ po) A cᴾ
Lemma-3-5-a = RS42.RS42a
Lemma-3-5-b
  : {ℓΦ ℓΨ ℓΦ' ℓΨ' ℓP : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Φ' : UUᵉ ℓΦ'} {Ψ' : UUᵉ ℓΨ'}
    (i : Φ → Ψ) (i' : Φ' → Ψ') {P : UUᵉ ℓP} (inlᴾ : Φ ×ᵉ Ψ' → P) (inrᴾ : Ψ ×ᵉ Φ' → P)
    (glueᴾ : (w : Φ ×ᵉ Φ') → inlᴾ (RS42.pp-left i i' w) =ᵉ inrᴾ (RS42.pp-right i i' w))
    (po : {ℓE : Level} →
      ExoPushout.is-exo-pushout (RS42.pp-left i i') (RS42.pp-right i i') inlᴾ inrᴾ glueᴾ ℓE)
    {ℓA : Level} (A : Ψ ×ᵉ Ψ' → UUᵉ ℓA) (cᴾ : (p : P) → A (RS42.i□i' i i' inlᴾ inrᴾ glueᴾ po p)) →
    Core.Ext (RS42.i□i' i i' inlᴾ inrᴾ glueᴾ po) A cᴾ
    ≅ Core.Ext i' (RS42.E₂ i i' inlᴾ inrᴾ glueᴾ po A cᴾ) (RS42.c₂ i i' inlᴾ inrᴾ glueᴾ po A cᴾ)
Lemma-3-5-b = RS42.RS42b

-- Lemma 3.6: Σ-splitting,  Extᵢ of a Σ-family  ≅  Σ of iterated extension types.
Lemma-3-6
  : {ℓΦ ℓΨ ℓX ℓY : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (X : Ψ → UUᵉ ℓX)
    (Y : (ψ : Ψ) → X ψ → UUᵉ ℓY) (a : (φ : Φ) → X (i φ)) (b : (φ : Φ) → Y (i φ) (a φ)) →
    Core.Ext i (λ ψ → Σᵉ (X ψ) (Y ψ)) (λ φ → a φ ,ᵉ b φ)
    ≅ Σᵉ (Core.Ext i X a)
        (λ f → Core.Ext i (λ ψ → Y ψ (Lemma-3-2-eval f ψ))
          (λ φ → exo-tr (Y (i φ)) (exo-inv (Lemma-3-2-bdry f φ)) (b φ)))
Lemma-3-6 = RS.RS43

-- Lemma 3.7: extension along a composite of cofibrations, in two steps.
Lemma-3-7
  : {ℓΦ ℓΨ ℓΩ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Ω : UUᵉ ℓΩ} (i : Φ → Ψ) (j : Ψ → Ω)
    (A : Ω → UUᵉ ℓA) (a : (φ : Φ) → A (j (i φ))) →
    Core.Ext (λ φ → j (i φ)) A a
    ≅ Σᵉ (Core.Ext i (λ ψ → A (j ψ)) a) (λ f → Core.Ext j A (Lemma-3-2-eval f))
Lemma-3-7 = RS.RS44

-- Lemma 3.8: union of cofibrations.  Conditionally formalized: parametrized by an
-- assumed meet M ("Φ∧Ψ", two maps u, v) and an assumed outer pushout P ("Φ∨Ψ") with strict
-- UMP (`interface-exo-pushout` below), the paper's hypotheses ("assumed when they exist").
-- The iso itself uses no cofibration/fibrancy hypotheses; those matter only for the
-- well-formedness discussion, as in the paper.
Lemma-3-8
  : {ℓM ℓΦ ℓΨ ℓP ℓA : Level} {M : UUᵉ ℓM} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (u : M → Φ) (v : M → Ψ)
    {P : UUᵉ ℓP} (inlᴾ : Φ → P) (inrᴾ : Ψ → P) (glueᴾ : (m : M) → inlᴾ (u m) =ᵉ inrᴾ (v m))
    (A : P → UUᵉ ℓA) (a : (ψ : Ψ) → A (inrᴾ ψ))
    (po : ExoPushout.is-exo-pushout u v inlᴾ inrᴾ glueᴾ ℓA) →
    Core.Ext inrᴾ A a ≅ Core.Ext u (λ x → A (inlᴾ x)) (RS45.a∧ u v inlᴾ inrᴾ glueᴾ A a)
Lemma-3-8 = RS45.RS45

-- Lemma 3.11: relative function extensionality, pointwise contractible implies the
-- extension type is contractible.  (In the restructured paper, Lemma 3.11 now denotes the merged
-- lemma: Lemma 3.11 and Lemma 3.11 are two labels on one environment, the statement
-- indexed as Lemma-3-11 above.)  For a full 2LTT cofibration this is Lemma-3-11 (no
-- cofibrancy); `RS46.RS46` is the cofibrant-shapes proof from the fibration half alone (the
-- lemma discharging the trivial half).  Plus the purely strict form (strictly contractible
-- fibres give a strictly contractible Ext).
Lemma-3-11-contr
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ)
    (cY : (ψ : Ψ) → is-contr (Y ψ)) (a : (φ : Φ) → C (Y (i φ))) →
    Fib-is-contr (Core.Ext i (λ ψ → C (Y ψ)) a) {CofibFibration.Ext-isFibrant cof Y a}
Lemma-3-11-contr        = RS46.RS46
Lemma-3-11-full
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ) →
    Definition-3-9 (pr1ᵉ c2)
Lemma-3-11-full   = RelFunext.rel-funext-holds-2LTT
Lemma-3-11-strict
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {A : Ψ → UUᵉ ℓA}
    (a : (φ : Φ) → A (i φ)) (cA : (ψ : Ψ) → Core.is-contrᵉ (A ψ)) →
    Core.is-contrᵉ (Core.Ext i A a)
Lemma-3-11-strict = RSHomotopy.Ext-strict-contr

-- Lemma 3.13: extension extensionality in the paper's homotopy form. The
-- canonical happly map identifies the identity type of the fibrant match of
-- Ext with the match of the extension type of pointwise paths restricting to
-- reflexivity. The strict outer identity is retained separately below.
Lemma-3-13
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
    (f g : RS48Ext.EA (pr1ᵉ c2) (pr2ᵉ c2) Y a) →
    Id f g ≃ RS48Ext.Q (pr1ᵉ c2) (pr2ᵉ c2) Y a f g
Lemma-3-13 c2 = RS48Ext.RS48Ext (pr1ᵉ c2) (pr2ᵉ c2)

Lemma-3-13-strict
  : {ℓΦ ℓΨ ℓA : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {A : Ψ → UUᵉ ℓA}
    {a : (φ : Φ) → A (i φ)} (f g : Core.Ext i A a) →
    (f =ᵉ g)
    ≅ Core.Ext i (λ ψ → Lemma-3-2-eval f ψ =ᵉ Lemma-3-2-eval g ψ)
        (λ φ → exo-concat (Lemma-3-2-bdry f φ) (exo-inv (Lemma-3-2-bdry g φ)))
Lemma-3-13-strict = RS48.Ext-Id-strict

-- Lemma 3.14: the full homotopy extension property.  A weakly agreeing
-- section is replaced by a strict extension a', together with a homotopy
-- whose restriction is strictly the original boundary homotopy, after the
-- explicit transport required by propositional strict equality.  The full
-- cofibration hypothesis supplies both the fibration and relative-function-
-- extensionality halves; no cofibrancy of Φ or Ψ is assumed.
Lemma-3-14
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) → RS411.HEP (pr1ᵉ c2)
Lemma-3-14 c2 = RS411.HEP-holds (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-agrees
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ))
    (a : (φ : Φ) → C (Y (i φ))) (e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ)))) (ψ : Ψ) →
    Id (ic (Lemma-3-2-eval (Lemma-3-14-strictify c2 Y b a e) ψ)) (ic (b ψ))
Lemma-3-14-agrees c2 = RS410.a'-agrees-b (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-full
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) → RS411.HEP (pr1ᵉ c2)
Lemma-3-14-full c2 = RS411.HEP-holds (pr1ᵉ c2) (pr2ᵉ c2)
Lemma-3-14-pack
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (c2 : RelFunext.is-cofib-2LTT i ℓ)
    (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ))
    (a : (φ : Φ) → C (Y (i φ))) (e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ)))) →
    RS410Pack.HEP (pr1ᵉ c2) (pr2ᵉ c2) Y b a e
Lemma-3-14-pack c2 = RS410Pack.hep (pr1ᵉ c2) (pr2ᵉ c2)

-- RS 4.11, the consistency check Section 3 mentions: (RS 4.10 + naive RS 4.8)
-- ⇒ RS 4.6.  Formalized as a
-- parametrized implication, not a re-derivation of RS 4.6: for a fixed i carrying only the
-- fibration half `is-cofib` (needed just to speak of fibrant matches), the two hypotheses are
-- parameters, `RS411.HEP` (RS 4.10, both components) and `RS411.NaiveExtExt` (naive RS 4.8,
-- in the rendering of Extension.RS48Ext), and the conclusion is `satisfies-rel-funext`
-- (RS 4.6, Definition-3-9).  For cofibrant shapes both hypotheses are discharged in the
-- framework (`RS411-hyp-HEP`, `RS411-hyp-NEE`), so RS 4.6 is recovered through the implication
-- (`RS411-check`), the paper's consistency check.
RS411-implication
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ) →
    RS411.HEP cof → RS411.NaiveExtExt cof → Definition-3-9 cof
RS411-implication       = RS411.RS411
RS411-hyp-HEP
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) →
    RS411.HEP cof
RS411-hyp-HEP cof cofΨ cofΦ =
  RS411.HEP-holds cof (RelFunext.rel-funext-holds cof cofΨ cofΦ)
RS411-hyp-NEE
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) →
    RS411.NaiveExtExt cof
RS411-hyp-NEE cof cofΨ cofΦ =
  RS411.NaiveExtExt-holds cof (RelFunext.rel-funext-holds cof cofΨ cofΦ)
RS411-check
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) →
    Definition-3-9 cof
RS411-check cof cofΨ cofΦ =
  RS411.rs46-recovered cof (RelFunext.rel-funext-holds cof cofΨ cofΦ)

-- Lemma 3.15: truncation levels, if every fibre A ψ is an n-type then so is the
-- extension type.  Propositional case (needs no funext), and the general case for all n.
Lemma-3-15-props
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : CofibFibration.is-cofib i ℓ)
    (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ))) →
    ((ψ : Ψ) → is-prop (Y ψ)) →
    Fib-is-prop (Core.Ext i (λ ψ → C (Y ψ)) a) {CofibFibration.Ext-isFibrant cof Y a}
Lemma-3-15-props   = RS412.Ext-is-prop
Lemma-3-15-general
  : {ℓΦ ℓΨ ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i ℓ) (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
    (t : RS412Ext.TruncationLevelᵉ) →
    ((ψ : Ψ) → is-type (RS412Ext.decode-level t) (Y ψ)) →
    is-type (RS412Ext.decode-level t) (fibrant-match (CofibFibration.Ext-isFibrant (pr1ᵉ c2) Y a))
Lemma-3-15-general c2 = RS412Ext.Ext-truncation (pr1ᵉ c2) (pr2ᵉ c2)


----------------------------------------------------------------------------------------------------
{- §4  Gluing -}
----------------------------------------------------------------------------------------------------

-- Definition 4.1, "The CCHM rules on sections": the paper's rendering of all seven displayed
-- CCHM operations, asserted in the ambient context. `literal-glue-rules` fixes one input, the
-- intermediate predicate quantifies over inputs for one cofibration, and `CCHMGlue`
-- quantifies over full cofibrations at arbitrary levels. Items (1) to (3) are generic; items
-- (4) to (7) are recorded at the ambient context only, so this does not encode the closure of
-- the element-level rules under substitution that a primitive contextual CCHM type former
-- would have. The paper states that gap in the paragraph after the definition.
-- Items (1) through (3), plus pointwise invertibility of unglue, are certified
-- to agree with the homotopy form by `Definition-4-1-bridge`.
Definition-4-1-at
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ))) →
    UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-1-at = GlueLiteralRules.literal-glue-rules
Definition-4-1
  : (𝓤 : Level) → SSetω
Definition-4-1 = GlueLiteralRules.CCHMGlue
Definition-4-1-at-cofibration
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} →
    (Φ → Ψ) → (𝓤 : Level) → UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-1-at-cofibration = GlueLiteralRules.satisfies-literal-glue-rules
Definition-4-1-bridge
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {𝓤 : Level} (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
    (r : Definition-4-1-at i 𝓤 A T f) →
    ((ψ : Ψ) → C (isEquiv (GlueLiteralRules.literal-glue-rules.unglue r ψ))) →
    Σᵉ (Ψ → UU 𝓤)
      (λ Gl → Σᵉ ((λ φ → Gl (i φ)) =ᵉ T)
        (λ p → Σᵉ ((ψ : Ψ) → Gl ψ → A ψ)
          (λ ung → Σᵉ
            ((φ : Φ) →
              c (ung (i φ)) =ᵉ exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
              (λ ξ → c (pr1 (ic (f ξ)))) φ) (λ _ → (ψ : Ψ) → C (isEquiv (ung ψ))))))
Definition-4-1-bridge    = GlueLiteralRules.literal-to-homotopy-rules-at

-- Remark 4.4: the homotopy form of the Glue rules, a family Gl,
-- a strict boundary Gl∘i =ᵉ T, an unglue with strict boundary behaviour, and each unglue_ψ an
-- equivalence.
Remark-4-4-homotopy-form
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) → UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Remark-4-4-homotopy-form = GlueRules.satisfies-homotopy-glue-rules

-- Lemma 4.2: the constructor package inverts the restriction-unglue
-- comparison map Θ(b) = (b∘i via p, unglue⊙b).
--   (1) the element-level rules, items (4)–(7) of Definition 4.1, hold iff Θ admits a strict
--       two-sided inverse (purely formal, no cofibrancy);
--   (2) with Φ cofibrant and unglue pointwise an equivalence (the homotopy form), Θ-hat is an
--       equivalence and the package holds up to homotopy with strict term boundary:
--       glue-tm / glue-strict-bdry / linked β and η paths / contractible uniqueness;
--   where the paper's Step A cites RS 4.8 at Φ = ∅, the formalization uses the cofibrant-
--   product funext PiTruncation.funext-Id-equiv (same content).
Lemma-4-2-i-to
  : {ℓφ ℓΨ : Level} {Φ : 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 ξ)))) φ) →
    (GlueLiteralRules.GlueNotation.ConstructorPackage i 𝓤 A T f G p ung ubd →
      GlueConstructorPackage.StrictInverse i A T f G p ung ubd)
    ×ᵉ
    (GlueConstructorPackage.StrictInverse i A T f G p ung ubd →
      GlueLiteralRules.GlueNotation.ConstructorPackage i 𝓤 A T f G p ung ubd)
Lemma-4-2-i-to i A T f G p ung ubd =
  GlueConstructorPackage.package-to-inverse i A T f G p ung ubd ,ᵉ
  GlueConstructorPackage.inverse-to-package i A T f G p ung ubd
Lemma-4-2-i-from
  : {ℓφ ℓΨ : Level} {Φ : 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 ξ)))) φ) →
    GlueConstructorPackage.StrictInverse i A T f G p ung ubd →
    GlueLiteralRules.GlueNotation.ConstructorPackage i 𝓤 A T f G p ung ubd
Lemma-4-2-i-from    = GlueConstructorPackage.inverse-to-package
-- The paper assumes only that Φ is cofibrant.  Cofibrancy of Ψ is derived
-- from the full cofibration i and kept abstract so large matched presentations
-- do not repeatedly normalize the closure proof.
abstract
  Lemma-4-2-cofΨ
    : {ℓS 𝓤 : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ} →
      RelFunext.is-cofib-2LTT i 𝓤 → isCofibrant Φ 𝓤 → isCofibrant Ψ 𝓤
  Lemma-4-2-cofΨ = CofibClosure.cofib-codomain-cofibrant

Lemma-4-2-ii
  : {ℓS 𝓤 : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i 𝓤)
    (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 ξ)))) φ)
    (inv : (ψ : Ψ) → C (isEquiv (ung ψ))) →
    GlueConstructorPackage.ThetaAnalysis.Package2.HomotopyConstructorPackage
      (pr1ᵉ c2) cofΦ (Lemma-4-2-cofΨ c2 cofΦ)
      A T f G p ung ubd inv
Lemma-4-2-ii c2 cofΦ =
  GlueConstructorPackage.ThetaAnalysis.Package2.homotopy-constructor-package
    (pr1ᵉ c2) cofΦ (Lemma-4-2-cofΨ c2 cofΦ)

Lemma-4-2-iii
  : {ℓS 𝓤 : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
    (c2 : RelFunext.is-cofib-2LTT i 𝓤)
    (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 ξ)))) φ) →
    GlueConstructorPackage.StrictInverse i A T f G p ung ubd →
    isEquiv
      (GlueConstructorPackage.ThetaAnalysis.unglue-match
        (pr1ᵉ c2) cofΦ (Lemma-4-2-cofΨ c2 cofΦ)
        A T f G p ung ubd)
Lemma-4-2-iii c2 cofΦ =
  GlueConstructorPackage.ThetaAnalysis.unglue-equiv-of-strict-inverse
    (pr1ᵉ c2) cofΦ (Lemma-4-2-cofΨ c2 cofΦ)

-- Remark 4.4: the homotopy Glue rules (the homotopy form above) hold iff a
-- strictly coherent Glue structure exists, and the two kinds of data differ only in their
-- propositional isEquiv components.  Direction "strictly coherent ⇒ rules" needs no hypotheses
-- and takes underlying maps definitionally; direction "rules ⇒ strictly coherent" strictly
-- realigns the isEquiv witnesses (the Corollary 3.12 instance, proved directly via relative
-- funext) and preserves the underlying unglue maps definitionally.  Hypotheses: the two halves
-- of the full 2LTT cofibration; no cofibrancy of Φ or Ψ.  The contractible uniqueness of the
-- realignment (the final clause of Corollary 3.12) is not part of this packaging, only
-- existence.
Remark-4-4
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {𝓤 : Level}
    (cof : CofibFibration.is-cofib i 𝓤) (triv : Definition-3-9 cof) →
    (Remark-4-4-homotopy-form i 𝓤 → GlueStructure.has-strictly-coherent-glue i 𝓤)
      ×ᵉ
      (GlueStructure.has-strictly-coherent-glue i 𝓤 →
        Remark-4-4-homotopy-form i 𝓤)
Remark-4-4           = GlueHomotopySemantic.homotopy-vs-semantic
Remark-4-4-to-strict
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {𝓤 : Level}
    (cof : CofibFibration.is-cofib i 𝓤) (triv : Definition-3-9 cof) →
    Remark-4-4-homotopy-form i 𝓤 → GlueStructure.has-strictly-coherent-glue i 𝓤
Remark-4-4-to-strict = GlueHomotopySemantic.homotopy-rules-to-strict-coh
Remark-4-4-to-rules
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) →
    GlueStructure.has-strictly-coherent-glue i 𝓤 → Remark-4-4-homotopy-form i 𝓤
Remark-4-4-to-rules  = GlueHomotopySemantic.strict-coh-to-homotopy-rules


-- coherence built in (one concept; GlueData = the type of Glue structures per input): paper
-- Definition 4.3 = `GlueOutput` + `is-strictly-coherent`, i.e. `has-strictly-coherent-glue` /
-- `GlueData` below.  The Agda module keeps the uncoherent output triple and the up-to-path
-- coherence (`is-homotopy-coherent`) as separate predicates: the former is the carrier, the
-- latter is the weakened variant consumed by Lemma 5.13(2) and covered by Remark 5.16.
Definition-4-3-output
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-3-output       = GlueStructure.GlueOutput
Definition-4-3-strict-coh
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    Definition-4-3-output i 𝓤 A T e → UUᵉ (ℓφ ⊔ 𝓤)
Definition-4-3-strict-coh   = GlueStructure.is-strictly-coherent
Definition-4-3-homotopy-coh
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    Definition-4-3-output i 𝓤 A T e → UUᵉ (ℓφ ⊔ 𝓤)
Definition-4-3-homotopy-coh = GlueStructure.is-homotopy-coherent
Definition-4-3-fixed-data
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-3-fixed-data = GlueStructure.GlueData
Definition-4-3-has
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) → UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-3-has          = GlueStructure.has-glue-structure
Definition-4-3-data
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) → UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-3-data = GlueStructure.has-strictly-coherent-glue
Definition-4-3-has-homotopy
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) → UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-4-3-has-homotopy = GlueStructure.has-homotopy-coherent-glue





----------------------------------------------------------------------------------------------------
{- §5  The equivalence of Gluing and Univalence -}
-- The paper's "contractible Glue data" and "equivalence cycle" appear as `strong` and
-- `sandwich` in the Agda names below.
----------------------------------------------------------------------------------------------------

-- Lemma 5.1: the type of Glue data is an extension type,
--     GlueData_{i,𝓤}(A , T , e)  ≅  Extᵢ(W , w₀)   for   W ψ = Σ (X : 𝓤) . (X ≃ A ψ),
-- hence fibrant when i is a cofibration.
Lemma-5-1
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) →
    (Definition-4-3-fixed-data i 𝓤 A T e
      ≅ Core.Ext i (λ ψ → C (GlueStructure.W i 𝓤 A ψ))
          (λ φ → c {A = GlueStructure.W i 𝓤 A (i φ)} (T φ , ic (e φ))))
    ×ᵉ isFibrant (Definition-4-3-fixed-data i 𝓤 A T e)
Lemma-5-1 i 𝓤 A T e cof =
  GlueDataFibrant.glue-data-≅ i 𝓤 A T e ,ᵉ
  GlueDataFibrant.GlueData-isFibrant i 𝓤 A T e cof

Lemma-5-1-iso
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    Definition-4-3-fixed-data i 𝓤 A T e
    ≅ Core.Ext i (λ ψ → C (GlueStructure.W i 𝓤 A ψ))
        (λ φ → c {A = GlueStructure.W i 𝓤 A (i φ)} (T φ , ic (e φ)))
Lemma-5-1-iso = GlueDataFibrant.glue-data-≅
Lemma-5-1-fibrant
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    CofibFibration.is-cofib i (lsuc 𝓤) → isFibrant (Definition-4-3-fixed-data i 𝓤 A T e)
Lemma-5-1-fibrant = GlueDataFibrant.GlueData-isFibrant

-- Definition 5.2: contractible Glue data (the Agda identifiers keep `strong`).  For every input
-- (A,T,e) the type GlueData_{i,𝓤}(A,T,e) is contractible as a fibrant type, i.e. inner `is-contr`
-- of the fibrant match supplied by Lemma-5-1-fibrant ("a meaningful demand by Lemma 5.1").  The
-- definition accordingly carries the fibrancy input (the fibration half of the cofibration).
Definition-5-2
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) →
    UUᵉ ((ℓφ ⊔ ℓΨ) ⊔ lsuc 𝓤)
Definition-5-2 = GlueDataFibrant.has-strong-glue-structure

-- Remark 5.3: reading of Definition 5.2 (contractible Glue data = an internal, strictified
-- equivalence extension property: every strict fibre of the restriction map R_A is contractible;
-- under Lemma-5-1's Ext presentation, R_A is the restriction fibration i*_W).  The identification
-- it describes is the route formalized in Theorem-5-4 below.

-- Theorem 5.4: The strong direction.  Univalence gives a strong Glue
-- structure for every full 2LTT cofibration, no cofibrancy of Φ or Ψ.  The proof is the
-- trivial-fibration half (relative funext, Lemma 3.11) applied to the pointwise-contractible glue
-- family W.  Stated in the paper's packaging (Definition 5.2, `ua-strong-glue`), in the raw
-- extension-type form (`ua-implies-strong-glue`), in the GlueData form (`ua-glue-data-contr`,
-- definitionally the same statement as Definition 5.2), and in the earlier cofibrant-shapes form
-- (trivial half discharged by RS46).
Theorem-5-4
  : {ℓΦ ℓΨ 𝓤 : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) (triv : Definition-3-9 cof) →
    Definition-5-2 i 𝓤 cof
Theorem-5-4           = GlueSandwich.ua-strong-glue
Theorem-5-4-Ext
  : {ℓΦ ℓΨ 𝓤 : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) →
    Definition-3-9 cof →
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    is-contr
      (fibrant-match
        (CofibFibration.Ext-isFibrant cof (UAStrongGlue.GlueFam A) (λ φ → c (T φ , ic (e φ)))))
Theorem-5-4-Ext       = UAStrongGlue.ua-implies-strong-glue
Theorem-5-4-GlueData
  : {ℓΦ ℓΨ 𝓤 : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) →
    Definition-3-9 cof →
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    is-contr (fibrant-match (Lemma-5-1-fibrant i 𝓤 A T e cof))
Theorem-5-4-GlueData  = GlueSandwich.ua-glue-data-contr
Theorem-5-4-cofibrant
  : {ℓΦ ℓΨ 𝓤 : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (cof : CofibFibration.is-cofib i (lsuc 𝓤)) →
    isCofibrant Ψ (lsuc 𝓤) →
    isCofibrant Φ (lsuc 𝓤) →
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) →
    is-contr
      (fibrant-match
        (CofibFibration.Ext-isFibrant cof (UAStrongGlue.GlueFam A) (λ φ → c (T φ , ic (e φ)))))
Theorem-5-4-cofibrant = UAStrongGlue.ua-implies-strong-glue-cofibrant

-- Corollary 5.5, including all conclusions.  Since Agda's cofibration
-- predicate is indexed by the tested universe, the small instance is used by
-- Lemma 4.2 and the successor-level instance by contractibility of Glue data.
-- The paper's unindexed cofibration and cofibrancy hypotheses supply both.
Corollary-5-5
  : {ℓS 𝓤 : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (c2-small : RelFunext.is-cofib-2LTT i 𝓤)
    (c2-large : RelFunext.is-cofib-2LTT i (lsuc 𝓤))
    (cofΦ-small : isCofibrant Φ 𝓤)
    (cofΦ-large : isCofibrant Φ (lsuc 𝓤)) →
    Corollary55.Corollary55 i (pr1ᵉ c2-small) (pr1ᵉ c2-large)
      cofΦ-small cofΦ-large
Corollary-5-5 = Corollary55.univalence-gives-homotopy-form

-- Definition 5.6: clause (1), an interval, is the shape I with
-- boundary inclusion i∂ : 1+1 → I a full 2LTT cofibration; clause (2), a line-to-identity
-- structure, sends a line g : I → Y to an inner path g 0 = g 1, naturally in Y up to inner
-- equality.  Endpoint compatibility is part of the codomain of `path`, so it needs no field,
-- and no comparison in the other direction is assumed.  Clause (2) quantifies over fibrant Y
-- "of arbitrary size" in the paper, which is what lets the bridges below instantiate it one
-- level up; the record therefore takes the test level as a parameter rather than fixing it.
-- `PathStructure` is clause (2) at the
-- level the coercion laws need; degeneracy on constant lines is *derived* there from
-- naturality at Y = ⊤ (the Lemma 5.8 (c3) derivation), not assumed.
Definition-5-6
  : (ℓI 𝓤 : Level) → UUᵉ (lsuc ℓI ⊔ lsuc 𝓤)
Definition-5-6         = Conservativity.PathInterval
Definition-5-6-presentation
  : (ℓI 𝓤 : Level) → UUᵉ (lsuc (ℓI ⊔ 𝓤))
Definition-5-6-presentation = Conservativity.PathPresentation
Definition-5-6-aligned
  : (ℓI 𝓤 : Level) → UUᵉ (lsuc ℓI ⊔ lsuc (lsuc 𝓤))
Definition-5-6-aligned = CoercionLaws.PathStructure
Definition-5-6-bridge
  : {ℓI 𝓤 : Level} (𝕀 : Definition-5-6 ℓI (lsuc 𝓤)) →
    Definition-5-6-aligned ℓI 𝓤
Definition-5-6-bridge  = Conservativity.PathInterval-to-PathStructure

-- Lemma 5.8: a full path interval yields the coercion operation and laws
-- (c1) through (c3), packaged together at the linked declaration. The named
-- component declarations below expose the stronger PathStructure-level
-- formulation used by Theorem 5.14 and homotopy composition.  The three types at which
-- Theorem 5.14 instantiates the line-to-identity operation, and which Remark 5.16 now lists,
-- are 𝓤 itself, the function classifier Σ(X,Y:𝓤).(X → Y), and ⊤; they are `path-univ`, `U→`
-- and `!I` in Extension.CoercionLaws.
Lemma-5-8-coe
  : {ℓI 𝓤 : Level} (𝕀 : Definition-5-6 ℓI (lsuc 𝓤)) →
    CoercionLawsNamed.CoercionPackage
      (Definition-5-6-bridge 𝕀)
Lemma-5-8-coe 𝕀 = CoercionLawsNamed.coercion-package
  (Conservativity.PathInterval-to-PathStructure 𝕀)
Lemma-5-8-coe-structure
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤) →
    CoercionLawsNamed.CoercionPackage P
Lemma-5-8-coe-structure = CoercionLawsNamed.coercion-package
Lemma-5-8-c1
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤)
    (G : CoercionLaws.PathStructure.I P → UU 𝓤) (x : G (CoercionLaws.PathStructure.0I P)) →
    Id (CoercionLawsNamed.coe P G x) (pr1 (idtoeqv (CoercionLawsNamed.path-univ P G)) x)
Lemma-5-8-c1  = CoercionLawsNamed.coercion-law-c1
Lemma-5-8-c2
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤)
    (G H : CoercionLaws.PathStructure.I P → UU 𝓤)
    (θ : (t : CoercionLaws.PathStructure.I P) → G t → H t)
    (x : G (CoercionLaws.PathStructure.0I P)) →
    Id (θ (CoercionLaws.PathStructure.1I P) (CoercionLawsNamed.coe P G x))
      (CoercionLawsNamed.coe P H (θ (CoercionLaws.PathStructure.0I P) x))
Lemma-5-8-c2  = CoercionLawsNamed.coercion-law-c2
Lemma-5-8-c3
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤) (Y : UU 𝓤) (x : Y) →
    Id (CoercionLawsNamed.coe P (λ _ → Y) x) x
Lemma-5-8-c3  = CoercionLawsNamed.coercion-law-c3

-- Remark 5.9: for a fibrant interval the coercion laws are the standard
-- transport facts, so the interface of Theorem 5.14 is discharged with no extra assumptions.
-- The later claim that the point interval never has a cofibrant boundary is a
-- model-level assertion and is not represented by this internal declaration.
Remark-5-9
  : {ℓI : Level} (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁) →
    Definition-5-6-aligned ℓI 𝓤
Remark-5-9 = WeakGlueUAFibrant.fibrant-path-structure

-- Lemma 5.10: if every idtoeqv_{A,B} merely has a section, the universe is
-- univalent (via the fundamental theorem of identity types, retract-of-singleton form).
Lemma-5-10
  : {𝓤 : Level} (s : (A B : UU 𝓤) → A ≃ B → Id A B) →
    ((A B : UU 𝓤) (g : A ≃ B) → Id (idtoeqv (s A B g)) g) → (A B : UU 𝓤) → isEquiv idtoeqv
Lemma-5-10 = UAFromSection.ua-from-section

-- Definition 5.11: the sharply weakened Glue structure on an interval, a family
-- G : I → 𝓤, two paths G 0 = A, G 1 = B in the universe, mere maps, endpoint homotopies.
Definition-5-11
  : {ℓI : Level} (I : UUᵉ ℓI) (0I 1I : I) (𝓤 : Level) → UUᵉ (ℓI ⊔ lsuc 𝓤)
Definition-5-11 = GlueRules.WeakGlue

-- The weakenings of Definition 5.11 are visible in the formalized hypotheses: Definition-5-11
-- takes no cofibration, and Theorem-5-14 never inverts u.

-- Remark 5.12: univalence inhabits the weak structure (take G ≔ λ_.B,
-- b₀ ≔ ua(f)⁻¹, b₁ ≔ refl).
Remark-5-12
  : {ℓI : Level} (I : UUᵉ ℓI) (0I 1I : I) (𝓤 : Level) →
    Univalence.Univalence 𝓤 → Definition-5-11 I 0I 1I 𝓤
Remark-5-12 = GlueRules.ua-gives-weak-glue

-- Lemma 5.13, both clauses.  The public declaration packages the two
-- universally quantified implications and retains the cofibration hypotheses
-- stated in the paper.  The second proof does not use its cofibration witness,
-- which is the stronger fact observed in the proof.
Lemma-5-13-i
  : {ℓφ ℓΨ ℓI : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ}
    (i : Φ → Ψ) (I : UUᵉ ℓI) (i∂ : ⊤ᵉ +ᵉ ⊤ᵉ → I) (𝓤 : Level)
    (c2 : RelFunext.is-cofib-2LTT i (lsuc 𝓤))
    (c2∂ : RelFunext.is-cofib-2LTT i∂ (lsuc 𝓤)) →
    (Definition-5-2 i 𝓤 (pr1ᵉ c2) →
      Definition-4-3-data i 𝓤)
    ×ᵉ
    (Definition-4-3-has-homotopy i∂ 𝓤 →
      Definition-5-11 I (i∂ (inlᵉ starᵉ)) (i∂ (inrᵉ starᵉ)) 𝓤)
Lemma-5-13-i i I i∂ 𝓤 c2 _ =
  GlueDataFibrant.strong-to-strict i 𝓤 (pr1ᵉ c2) ,ᵉ
  GlueStrengthChain3.strength-chain-3 I i∂ 𝓤

Lemma-5-13-i-contractible-to-structure
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
    (c2 : RelFunext.is-cofib-2LTT i (lsuc 𝓤)) →
    Definition-5-2 i 𝓤 (pr1ᵉ c2) →
    Definition-4-3-data i 𝓤
Lemma-5-13-i-contractible-to-structure i 𝓤 c2 =
  GlueDataFibrant.strong-to-strict i 𝓤 (pr1ᵉ c2)
Lemma-5-13-ii
  : {ℓφ ℓΨ : Level} {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) (A : Ψ → UU 𝓤)
    (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ))) (out : Definition-4-3-output i 𝓤 A T e) →
    Definition-4-3-strict-coh i 𝓤 A T e out →
    Definition-4-3-homotopy-coh i 𝓤 A T e out
Lemma-5-13-ii  = GlueStructure.strict-coh-to-homotopy-coh
Lemma-5-13-iii
  : {ℓI : Level} (I : UUᵉ ℓI) (i∂ : ⊤ᵉ +ᵉ ⊤ᵉ → I) (𝓤 : Level)
    (hcg : Definition-4-3-has-homotopy i∂ 𝓤) →
    Definition-5-11 I (i∂ (inlᵉ starᵉ)) (i∂ (inrᵉ starᵉ)) 𝓤
Lemma-5-13-iii = GlueStrengthChain3.strength-chain-3

-- Theorem 5.14: weak Glue plus a line-to-identity structure, clause (2) of
-- Definition 5.6, implies univalence.  The linked declaration takes clause (2)
-- alone (`PathPresentation`), with no boundary-cofibration witness, which is the
-- paper's hypothesis.  Further declarations expose the same theorem over the
-- level-shifted `PathStructure` interface and over the raw coercion laws.
Theorem-5-14-from-laws
  : {ℓI : Level} (I : UUᵉ ℓI) (0I 1I : I) (𝓤 : Level) (coe : (G : I → UU 𝓤) → G 0I → G 1I)
    (path-univ : (G : I → UU 𝓤) → Id (G 0I) (G 1I))
    (c1 : (G : I → UU 𝓤) (x : G 0I) → Id (coe G x) (pr1 (idtoeqv (path-univ G)) x))
    (c2 : (G H : I → UU 𝓤) (θ : (t : I) → G t → H t) (x : G 0I) →
      Id (θ 1I (coe G x)) (coe H (θ 0I x))) (c3 : (Y : UU 𝓤) (x : Y) → Id (coe (λ _ → Y) x) x) →
    Definition-5-11 I 0I 1I 𝓤 → (A B : UU 𝓤) → isEquiv idtoeqv
Theorem-5-14-from-laws = WeakGlueUA.weak-glue-implies-ua
Theorem-5-14
  : {ℓI 𝓤 : Level}
    (P : Definition-5-6-presentation ℓI (lsuc 𝓤)) →
    Definition-5-11
      (Conservativity.PathPresentation.shape P)
      (Conservativity.PathPresentation.point0 P)
      (Conservativity.PathPresentation.point1 P) 𝓤 →
    Univalence.Univalence 𝓤
Theorem-5-14 P = CoercionLaws.general-weak-glue-implies-ua
  (Conservativity.PathPresentation-to-PathStructure P)
Theorem-5-14-structure
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤) →
    Definition-5-11 (CoercionLaws.PathStructure.I P)
      (CoercionLaws.PathStructure.0I P)
      (CoercionLaws.PathStructure.1I P) 𝓤 →
    Univalence.Univalence 𝓤
Theorem-5-14-structure = CoercionLaws.general-weak-glue-implies-ua

-- The exact five-node statement of Theorem 5.15 is
-- `Theorem-5-15-fibrant` below.  These two declarations retain earlier
-- three-node corollaries for a fibrant interval and for the aligned path
-- interface.  They use homotopy coherence as an intermediate weakening and
-- are not the linked theorem statement.
Theorem-5-15-three-node-fibrant
  : {ℓI : Level} (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁)
    (cof : CofibFibration.is-cofib (GlueSandwichComplete.i∂ 𝕀 a₀ a₁) (lsuc 𝓤))
    (triv : Definition-3-9 cof) →
    (GlueSandwichComplete.Cond1 𝕀 a₀ a₁ 𝓤 seg cof triv →
        GlueSandwichComplete.Cond4 𝕀 a₀ a₁ 𝓤 seg cof triv) ×ᵉ
      ((GlueSandwichComplete.Cond4 𝕀 a₀ a₁ 𝓤 seg cof triv →
          GlueSandwichComplete.Cond5 𝕀 a₀ a₁ 𝓤 seg cof triv) ×ᵉ
        (GlueSandwichComplete.Cond5 𝕀 a₀ a₁ 𝓤 seg cof triv →
          GlueSandwichComplete.Cond1 𝕀 a₀ a₁ 𝓤 seg cof triv))
Theorem-5-15-three-node-fibrant = GlueSandwichComplete.glue-sandwich
Theorem-5-15-three-node-general
  : {ℓI 𝓤 : Level} (P : Definition-5-6-aligned ℓI 𝓤)
    (cof : CofibFibration.is-cofib (GlueSandwichGeneral.i∂ P) (lsuc 𝓤))
    (triv : Definition-3-9 cof) →
    (GlueSandwichGeneral.Cond1 P cof triv → GlueSandwichGeneral.Cond4 P cof triv) ×ᵉ
      ((GlueSandwichGeneral.Cond4 P cof triv → GlueSandwichGeneral.Cond5 P cof triv) ×ᵉ
        (GlueSandwichGeneral.Cond5 P cof triv → GlueSandwichGeneral.Cond1 P cof triv))
Theorem-5-15-three-node-general = GlueSandwichGeneral.glue-sandwich

-- Theorem 5.15 as stated.  The PathInterval record supplies its full
-- boundary cofibration.  Node (2) is the large scheme AllStrongGlue, which
-- quantifies over arbitrary levels of both endpoint shapes.  The five fields
-- are the implications (1) to (2) to (3) to (4) to (5) to (1), with node (4)
-- the paper's strictly coherent Glue structure.
Theorem-5-15-fibrant
  : {ℓI 𝓤 : Level} (𝕀 : Definition-5-6 ℓI (lsuc 𝓤)) →
    GlueSandwichFull.ExactPathInterval.ExactFiveNodeCycle 𝕀
Theorem-5-15-fibrant =
  GlueSandwichFull.ExactPathInterval.exact-five-node-cycle
Theorem-5-15-general
  : {ℓI 𝓤' : Level} (P : Definition-5-6-aligned ℓI 𝓤')
    (cof : CofibFibration.is-cofib (GlueSandwichGeneral.i∂ P) (lsuc 𝓤'))
    (triv : Definition-3-9 cof) →
    GlueSandwichFull.GeneralInterval.ExactFiveNodeCycle P cof triv
Theorem-5-15-general =
  GlueSandwichFull.GeneralInterval.exact-five-node-cycle
Theorem-5-15-any-cofibration
  : {ℓΦ ℓΨ : Level} (𝓤 : Level) {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence.Univalence 𝓤)
    (c2 : RelFunext.is-cofib-2LTT i (lsuc 𝓤)) →
    Definition-5-2 i 𝓤 (pr1ᵉ c2)
Theorem-5-15-any-cofibration = GlueSandwichFull.strong-glue-any-cofibration


----------------------------------------------------------------------------------------------------
{- §6  Conclusions: Towards an equivalence of type theories -}
----------------------------------------------------------------------------------------------------

-- The flagship example (Introduction and §5.2): a cubical path from y₀ to y₁ is the
-- extension type of the endpoint data along the boundary inclusion i∂ : ∂I ↪ I.
CubicalPath-is-Ext
  : {ℓI 𝓤 : Level} → Definition-5-6 ℓI 𝓤 → (Y : UU 𝓤) → C Y → C Y → UUᵉ (ℓI ⊔ 𝓤)
CubicalPath-is-Ext = Conservativity.CubicalPath

-- Section 6 is not formalized, and cannot be: it speaks about theories rather
-- than inside one.  Conjecture 6.1 is about type theories, Definition 6.2
-- presents two of them as axiomatic extensions of a fixed 2LTT, and Theorem 6.3
-- asserts mutual interpretability.  Stating that needs the syntax of both
-- theories, an interpretation function and a soundness proof, which is a
-- different project.
--
-- The mathematics Theorem 6.3 is assembled from is indexed above:
--
--   (ua) ⇒ contractible Glue data along every cofibration   Theorem-5-4
--   contractible Glue data ⇒ a Glue structure               Lemma-5-13-i
--   a Glue structure at i∂ ⇒ weak Glue                      Lemma-5-13-iii
--   weak Glue + clause (2) of Definition 5.6 ⇒ (ua)         Theorem-5-14
--   the whole cycle                                         Theorem-5-15-fibrant
--
-- Read internally, the two directions are
-- `TheoryComparison.univalence-implies-glue` and
-- `interval-and-glue-imply-univalence`, over the three axiom schemes of
-- Definition 6.2 as closed types (`Conservativity.Axiom-ua`, `Axiom-glue`,
-- `Axiom-int`).  Those are implications between postulate types, not the theory
-- comparison itself.
--
-- Definition 6.2 also takes the outer level to be extensional MLTT, while the
-- outer level here has UIP and function extensionality but no equality
-- reflection; the paper notes that its results stay valid in the stronger
-- setting.



----------------------------------------------------------------------------------------------------
{- Gluing at fibrant shapes  (Section 5.3, stated in prose) -}
----------------------------------------------------------------------------------------------------

-- The paper states this only in prose, in the paragraph before Definition 5.11: at a fibrant
-- shape with a segment, clause (2) of Definition 5.6 is definable by ap_g(seg), so weak Glue
-- is equivalent to univalence there, with no cofibration and no strict equality in the
-- argument.  The two entries below prove that; `Remark-5-9` uses the same
-- `WeakGlueUAFibrant.fibrant-path-structure`.
fibrant-shape-weak-glue-is-ua
  : {ℓI : Level} (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁) →
    (Univalence.Univalence 𝓤 → Definition-5-11 (C 𝕀) (c a₀) (c a₁) 𝓤) ×ᵉ
    (Definition-5-11 (C 𝕀) (c a₀) (c a₁) 𝓤 → Univalence.Univalence 𝓤)
fibrant-shape-weak-glue-is-ua 𝕀 a₀ a₁ 𝓤 seg =
  GlueRules.ua-gives-weak-glue (C 𝕀) (c a₀) (c a₁) 𝓤 ,ᵉ
  WeakGlueUAFibrant.fibrant-weak-glue-implies-ua 𝕀 a₀ a₁ 𝓤 seg
fibrant-shape-weak-glue-is-ua-composite
  : {ℓI : Level} (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁) →
    Definition-4-3-has-homotopy (GlueSandwichFibrant.i∂ 𝕀 a₀ a₁ 𝓤 seg) 𝓤 →
    (A B : UU 𝓤) →
    isEquiv idtoeqv
fibrant-shape-weak-glue-is-ua-composite = GlueSandwichFibrant.htpy-coherent-glue-implies-ua


{- References:

  [2LTT-Agda]  Elif Uskuplu.  2LTT-Agda: formalization of 2LTT in Agda.
               https://github.com/ElifUskuplu/2LTT-Agda, commit b064091 (6 August 2025).
               Described in: Elif Uskuplu, Formalizing two-level type theory with
               cofibrant exo-nat, Mathematical Structures in Computer Science 35:e30,
               2025.  doi:10.1017/S0960129525100297

  [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

  [Rzk]        Nikolai Kudasov and others.  Rzk proof assistant, since 2023.
               https://github.com/rzk-lang/rzk

  [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

  [Zhang]      Tesla Zhang.  Three non-cubical applications of extension types.
               arXiv:2311.05658, 2023.

  [Sterling]   Jonathan Sterling.  First steps in synthetic Tait computability: the
               objective metatheory of cubical type theory.  PhD thesis, Carnegie
               Mellon University, 2021 (CMU-CS-21-142).
               Jonathan Sterling and Robert Harper.  Logical relations as types:
               proof-relevant parametricity for program modules.  Journal of the ACM
               68(6):1-47, 2021.  doi:10.1145/3474834

  [Gratzer et al.]
               Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand and
               Lars Birkedal.  Controlling unfolding in type theory.  Mathematical
               Structures in Computer Science 35:e38, 2025.
               doi:10.1017/S0960129525100327

  [CCHM]       Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg.
               Cubical type theory: a constructive interpretation of the univalence
               axiom.  TYPES 2015, LIPIcs 69, 5:1-5:34, 2018.
               doi:10.4230/LIPIcs.TYPES.2015.5

-}