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

--------------------------------------------------------------------------------
-- Theorem 5.4 in the GlueData form: closing (1)⇒(2) of the
-- sandwich.
--
-- `UAStrongGlue.ua-implies-strong-glue` proves that the extension type
-- Extᵢ(W,w₀) has a contractible match; `GlueDataFibrant.GlueData-isFibrant`
-- makes GlueData fibrant with *the same* match (via `isFibrant-iso`, which keeps
-- the fibrant match on transferring fibrancy along `glue-data-≅`).  Hence, for a
-- univalent 𝓤 and a full 2LTT cofibration, the fibration half `cof` plus the
-- trivial half `triv` (relative funext); no cofibrancy of Φ or Ψ, the fibrant
-- type of Glue data is contractible for every input: the strong Glue structure
-- of Definition 5.2, in the form that Definition 4.3 demands.
--------------------------------------------------------------------------------

module Extension.GlueSandwich where

open import Extension.Prelude
open import Extension.CofibFibration using (is-cofib)
open import Extension.Univalence using (Univalence)
open import Extension.RelFunext using (satisfies-rel-funext)
open import Extension.GlueStructure
  using (has-homotopy-coherent-glue ; strict-coh-to-homotopy-coh)
open import Extension.GlueDataFibrant
  using (GlueData-isFibrant ; has-strong-glue-structure ; strong-to-strict)
open import Extension.UAStrongGlue using (ua-implies-strong-glue)

private
  variable
    ℓΦ ℓΨ 𝓤 : Level

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

  -- Univalence makes the (fibrant) type of Glue data contractible.
  ua-glue-data-contr :
      (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    → is-contr (fibrant-match (GlueData-isFibrant i 𝓤 A T e cof))
  ua-glue-data-contr A T e = ua-implies-strong-glue U cof triv A T e

  -- Theorem 5.4 in the paper's packaging: (i, 𝓤) has a strong
  -- Glue structure (Definition 5.2, Extension.GlueDataFibrant).  This is
  -- `ua-glue-data-contr` read at the definition.
  ua-strong-glue : has-strong-glue-structure i 𝓤 cof
  ua-strong-glue = ua-glue-data-contr

  -- (1)⇒(2)⇒(3)⇒(4): univalence gives a homotopy coherent Glue structure.
  -- Extract the centre of the contractible GlueData (a strictly coherent
  -- output, strength chain (1) = `strong-to-strict`) and coerce its strict
  -- coherence to a path (strength chain (2)).
  ua-homotopy-coherent-glue : has-homotopy-coherent-glue i 𝓤
  ua-homotopy-coherent-glue A T e =
    pr1ᵉ gd ,ᵉ strict-coh-to-homotopy-coh i 𝓤 A T e (pr1ᵉ gd) (pr2ᵉ gd)
    where
    gd = strong-to-strict i 𝓤 cof ua-strong-glue A T e