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

--------------------------------------------------------------------------------
-- Theorem 5.4.  Let i : Φ ↪ Ψ be a 2LTT cofibration and 𝓤 a fibrant univalent
-- universe.  Then
-- (i, 𝓤) has a strong Glue structure: for every input (A, T, e) the glue data
-- is contractible.  no cofibrancy of Φ or Ψ is needed: besides the fibration
-- half `cof`, the proof consumes only the trivial-fibration half of the
-- cofibration property, i.e. relative funext (`satisfies-rel-funext`,
-- Extension.RelFunext), matching the strengthened statement of the paper.
--
-- By Lemma 5.1 the glue data is the strict extension type
-- Extᵢ(W, w₀) of the *glue-data family*
--     W ψ ≔ Σ (X : 𝓤). (X ≃ A ψ)          (the types equipped with an
--                                           equivalence to A ψ)
-- with boundary  w₀ φ ≔ (T φ, e φ).  The proof is two steps:
--   Step 1 (univalence): each W ψ is contractible, it is a retract of the
--     singleton Σ(X). (X = A ψ) via idtoeqv and its section ua.
--   Step 2 (relative funext): the trivial half, applied to the trivially
--     fibrant family W, makes the match of Extᵢ(W, w₀) contractible.
-- (The universe level is bumped: W lives one level up, so the cofibration data
-- is taken at `lsuc 𝓤`.)
--
-- When Φ and Ψ are cofibrant, the trivial half is discharged by
-- `rel-funext-holds` (= Extension.RS46); that instance is
-- `ua-implies-strong-glue-cofibrant`.
--------------------------------------------------------------------------------

module Extension.UAStrongGlue where

open import Extension.Prelude
open import Extension.CofibFibration
open import Extension.RelFunext using (satisfies-rel-funext ; rel-funext-holds)
open import Extension.Univalence using (Univalence ; ua-from ; ua-from-β)

private
  variable
    ℓΦ ℓΨ 𝓤 : Level

-- The glue-data family: at ψ, the types X with an equivalence X ≃ A ψ.
GlueFam : {Ψ : UUᵉ ℓΨ} (A : Ψ → UU 𝓤) → Ψ → UU (lsuc 𝓤)
GlueFam {𝓤 = 𝓤} A ψ = Σ (UU 𝓤) (λ X → X ≃ A ψ)

-- Step 1.  Univalence makes each GlueFam A ψ contractible: it is a retract of
-- the contractible singleton Σ(X). (X = A ψ), the retraction being the
-- totalised idtoeqv and its section the totalised ua.
GlueFam-contr : {Ψ : UUᵉ ℓΨ} → Univalence 𝓤 → (A : Ψ → UU 𝓤) (ψ : Ψ)
              → is-contr (GlueFam A ψ)
GlueFam-contr {𝓤 = 𝓤} U A ψ =
  retract-of-singleton (Θ , (S , rs)) (path-type-is-contr (A ψ))
  where
  Θ : Σ (UU 𝓤) (λ X → Id X (A ψ)) → GlueFam A ψ
  Θ (X , p) = X , idtoeqv p
  S : GlueFam A ψ → Σ (UU 𝓤) (λ X → Id X (A ψ))
  S (X , g) = X , ua-from U g
  rs : (w : GlueFam A ψ) → Id (Θ (S w)) w
  rs (X , g) = dep-pair⁼ _ _ (refl , ua-from-β U g)

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (U    : Univalence 𝓤)
         (cof  : is-cofib i (lsuc 𝓤))
         (triv : satisfies-rel-funext cof)
       where

  -- Theorem 5.4: the glue-data extension type is contractible,
  -- for every input (A, T, e).  This is the trivial-fibration half (relative
  -- funext) on the univalence-contractible family GlueFam A.
  ua-implies-strong-glue :
      (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    → is-contr (fibrant-match
        (Ext-isFibrant cof (GlueFam A) (λ φ → c (T φ , ic (e φ)))))
  ua-implies-strong-glue A T e =
    triv (GlueFam A) (GlueFam-contr U A) (λ φ → c (T φ , ic (e φ)))

-- The earlier form: cofibrant Φ, Ψ discharge the trivial half (Extension.RS46).
ua-implies-strong-glue-cofibrant :
    {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U    : Univalence 𝓤)
    (cof  : is-cofib i (lsuc 𝓤))
    (cofΨ : isCofibrant Ψ (lsuc 𝓤))
    (cofΦ : isCofibrant Φ (lsuc 𝓤))
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
  → is-contr (fibrant-match
      (Ext-isFibrant cof (GlueFam A) (λ φ → c (T φ , ic (e φ)))))
ua-implies-strong-glue-cofibrant U cof cofΨ cofΦ =
  ua-implies-strong-glue U cof (rel-funext-holds cof cofΨ cofΦ)