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

--------------------------------------------------------------------------------
-- Lemma 5.1: the type of Glue data is an extension type.  For a 2LTT cofibration i and input
-- (A, T, e),
--
--     GlueData_{i,𝓤}(A,T,e)  ≅  Extᵢ(W, w₀),
--
-- the strict fibre of the restriction map for the universal glue-data family
--     W ψ = Σ(X:𝓤). (X ≃ A ψ),      w₀ φ = (T φ, e φ).
-- Univalence is not used.
--
-- The (G, u) ↔ w half is the strict Σ/Π-distributivity swap (round-trips are
-- `reflᵉ` by η).  The boundary half, the pair (β, coherence) versus the single
-- condition w∘i ≐ w₀, is handled by the exo-J maps `bdry-pt` / `bdry-pt-inv`;
-- both boundary spaces are strict propositions (spaces of `=ᵉ`-proofs), so the
-- round-trips are `UIPᵉ` on the proof components and `reflᵉ` on the data.
--
-- Since fibrancy of GlueData is established here, this module also hosts
-- Definition 5.2 (`has-strong-glue-structure`: contractibility of the
-- fibrant match of GlueData, for every input) and Lemma 5.13(1)
-- (`strong-to-strict`: extract the centre).
--------------------------------------------------------------------------------

module Extension.GlueDataFibrant where

open import Extension.Prelude
open import Extension.Core using (Ext ; ext-≡)
open import Extension.CofibFibration using (is-cofib ; Ext-isFibrant)
open import Extension.GlueStructure
  using (GlueData ; coerce-e ; W ; bdry-pt ; bdry-pt-inv ;
         has-strictly-coherent-glue)

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

-- Transport in a constant exo family is the identity.
exo-tr-const : {X : UUᵉ ℓ} {a b : X} {Y : UUᵉ ℓ'} (p : a =ᵉ b) (z : Y)
             → exo-tr (λ _ → Y) p z =ᵉ z
exo-tr-const reflᵉ z = reflᵉ

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
         (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
       where

  private
    w₀ : (φ : Φ) → C (W i 𝓤 A (i φ))
    w₀ φ = c {A = W i 𝓤 A (i φ)} (T φ , ic (e φ))

    ExtW : UUᵉ (ℓφ ⊔ ℓΨ ⊔ lsuc 𝓤)
    ExtW = Ext i (λ ψ → C (W i 𝓤 A ψ)) w₀

    to : GlueData i 𝓤 A T e → ExtW
    to ((G ,ᵉ (β ,ᵉ u)) ,ᵉ cc) =
      (λ ψ → c {A = W i 𝓤 A ψ} (G ψ , ic (u ψ)))
      ,ᵉ funextᵉ (λ φ → bdry-pt i 𝓤 A G T e u β cc φ)

    from : ExtW → GlueData i 𝓤 A T e
    from (w ,ᵉ p) =
      ((  (λ ψ → pr1 (ic (w ψ)))
       ,ᵉ (exo-ap (λ v φ → pr1 (ic (v φ))) p
       ,ᵉ (λ ψ → c (pr2 (ic (w ψ))))))
      ,ᵉ (λ φ → bdry-pt-inv i 𝓤 A w w₀ p φ))

    from-to : (g : GlueData i 𝓤 A T e) → from (to g) =ᵉ g
    from-to ((G ,ᵉ (β ,ᵉ u)) ,ᵉ cc) =
      dep-pair-=ᵉ _ _
        ( dep-pair-=ᵉ _ _
            (reflᵉ ,ᵉ dep-pair-=ᵉ _ _ (UIPᵉ _ _ ,ᵉ exo-tr-const _ u))
        ,ᵉ funextᵉ (λ φ → UIPᵉ _ _) )

    to-from : (x : ExtW) → to (from x) =ᵉ x
    to-from (w ,ᵉ p) = ext-≡ reflᵉ

  glue-data-≅ : GlueData i 𝓤 A T e ≅ ExtW
  glue-data-≅ = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))

  -- "Glue data form a fibrant type": transfer Extᵢ(W,w₀)'s fibrancy along the
  -- iso.  `isFibrant-iso` keeps the match, so `fibrant-match (GlueData-isFibrant
  -- cof)` is definitionally the match of Extᵢ(W,w₀), i.e. the type whose
  -- contractibility is `UAStrongGlue.ua-implies-strong-glue`.
  GlueData-isFibrant : is-cofib i (lsuc 𝓤) → isFibrant (GlueData i 𝓤 A T e)
  GlueData-isFibrant cof =
    isFibrant-iso (≅-sym glue-data-≅) (Ext-isFibrant cof (W i 𝓤 A) w₀)

  -- Centre-extraction plumbing: from contractibility of the (fibrant) GlueData
  -- match, produce an actual GlueData element (a strictly coherent output) by
  -- mapping the centre back through the fibrant witness.  This is what feeds the
  -- strength chain: strong Glue structure ⇒ strictly coherent output.
  strong-glue-centre : (cof : is-cofib i (lsuc 𝓤))
                     → is-contr (fibrant-match (GlueData-isFibrant cof))
                     → GlueData i 𝓤 A T e
  strong-glue-centre cof h =
    pr1ᵉ (pr2ᵉ (fibrant-witness (GlueData-isFibrant cof))) (c (pr1 h))

--------------------------------------------------------------------------------
-- Definition 5.2.  (i, 𝓤) has a strong Glue structure when, for every input
-- triple (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 provided by
-- `GlueData-isFibrant` (a meaningful demand by Lemma 5.1).  The
-- definition therefore carries the fibrancy input `cof` (the fibration half of
-- the cofibration property, at the level `lsuc 𝓤` of the glue-data family W).
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
         (cof : is-cofib i (lsuc 𝓤)) where

  has-strong-glue-structure : UUᵉ (ℓφ ⊔ ℓΨ ⊔ lsuc 𝓤)
  has-strong-glue-structure =
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    → is-contr (fibrant-match (GlueData-isFibrant i 𝓤 A T e cof))

  -- Lemma 5.13(1): a strong structure yields a strictly coherent
  -- one, extract the centre of the contractible match and map it back through
  -- the fibrant witness (`strong-glue-centre`).
  strong-to-strict : has-strong-glue-structure → has-strictly-coherent-glue i 𝓤
  strong-to-strict str A T e = strong-glue-centre i 𝓤 A T e cof (str A T e)