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

--------------------------------------------------------------------------------
-- Definition 4.3 (and its two coherence notions).
--
-- For a 2LTT cofibration i : Ξ¦ β†ͺ Ξ¨ and a fibrant universe (here the inner
-- universe `UU 𝓀`), a *Glue structure* sends every input triple
--
--   A : Ξ¨ β†’ 𝓀,   T : Ξ¦ β†’ 𝓀,   e : Ξ (Ο†). T Ο† ≃ A(iΟ†)
--
-- to an output triple
--
--   G : Ξ¨ β†’ 𝓀,   p : G∘i ≐ T,   u : Ξ (ψ). G ψ ≃ A ψ
--
-- (the top triangle commutes *strictly* via p; the bottom globe commutes up to
-- equivalence via u).  It is *strictly* / *homotopy* coherent if u restricts to
-- e up to strict / fibrant equality, comparing e along p (`coerce-e`).  For a
-- fixed input, `GlueData` is the type of quadruples (G,p,u,c) with c a strict
-- coherence witness.
--------------------------------------------------------------------------------

module Extension.GlueStructure where

open import Extension.Prelude

private
  variable
    β„“Ο† β„“Ξ¨ 𝓀 : Level

-- ΞΉ-fun : the paper's ΞΉ at a boundary, a strict equality of universe-valued
-- functions yields, pointwise, a path in the universe.  (One cannot form
-- `X =ᡉ Y` for universe elements directly, since `UU 𝓀` is not an exo type; but
-- a strict equality of *functions into* `UU 𝓀` lives on the exo function type,
-- and exo-J turns it into inner paths of the values.)
ΞΉ-fun : {Ξ¦ : UUᡉ β„“Ο†} (f g : Ξ¦ β†’ UU 𝓀) β†’ f =ᡉ g β†’ (Ο† : Ξ¦) β†’ Id (f Ο†) (g Ο†)
ΞΉ-fun f .f reflᡉ Ο† = refl

module _ {Ξ¦ : UUᡉ β„“Ο†} {Ξ¨ : UUᡉ β„“Ξ¨} (i : Ξ¦ β†’ Ξ¨) (𝓀 : Level) where

  -- Input triple (A, T, e).
  GlueInput : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
  GlueInput = Σᡉ (Ξ¨ β†’ UU 𝓀)
                 (Ξ» A β†’ Σᡉ (Ξ¦ β†’ UU 𝓀) (Ξ» T β†’ (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†))))

  module _ (A : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀) (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†))) where

    -- Output triple (G, p, u): item (1).
    GlueOutput : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
    GlueOutput = Σᡉ (Ξ¨ β†’ UU 𝓀)
                    (Ξ» G β†’ Σᡉ ((Ξ» Ο† β†’ G (i Ο†)) =ᡉ T)
                             (Ξ» _ β†’ (ψ : Ξ¨) β†’ C (G ψ ≃ A ψ)))

    -- e with its source coerced from T to G∘i along p  (writes e^p).  Transport
    -- in the *exo* family H ↦ Ξ (Ο†).C(H Ο† ≃ A(iΟ†)) over H : Ξ¦ β†’ UU 𝓀 (which is an
    -- exo type), avoiding an exo-transport indexed by the universe itself.
    coerce-e : (G : Ξ¨ β†’ UU 𝓀) β†’ (Ξ» Ο† β†’ G (i Ο†)) =ᡉ T β†’ (Ο† : Ξ¦) β†’ C (G (i Ο†) ≃ A (i Ο†))
    coerce-e G p = exo-tr (Ξ» H β†’ (Ο† : Ξ¦) β†’ C (H Ο† ≃ A (i Ο†))) (exo-inv p) e

    -- Item (3): strict coherence, u restricts to e up to strict equality.
    is-strictly-coherent : GlueOutput β†’ UUᡉ (β„“Ο† βŠ” 𝓀)
    is-strictly-coherent (G ,ᡉ (p ,ᡉ u)) = (Ο† : Ξ¦) β†’ u (i Ο†) =ᡉ coerce-e G p Ο†

    -- Item (2): homotopy coherence, u restricts to e up to fibrant equality.
    is-homotopy-coherent : GlueOutput β†’ UUᡉ (β„“Ο† βŠ” 𝓀)
    is-homotopy-coherent (G ,ᡉ (p ,ᡉ u)) =
      (Ο† : Ξ¦) β†’ C (Id (ic (u (i Ο†))) (ic (coerce-e G p Ο†)))

    -- GlueData_{i,𝓀}(A,T,e): quadruples (G,p,u,c) with c strict coherence.
    GlueData : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
    GlueData = Σᡉ GlueOutput is-strictly-coherent

    -- Lemma 5.13(2): strict coherence yields homotopy coherence,
    -- by coercing the strict equality to a fibrant path (`=ᡉ-to-Id`).
    strict-coh-to-homotopy-coh : (out : GlueOutput)
                               β†’ is-strictly-coherent out β†’ is-homotopy-coherent out
    strict-coh-to-homotopy-coh (G ,ᡉ (p ,ᡉ u)) coh Ο† = c (=ᡉ-to-Id (coh Ο†))

  -- A Glue structure / strictly-coherent Glue structure for (i, 𝓀):
  -- an output (resp. coherent quadruple) for every input triple.
  has-glue-structure : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
  has-glue-structure =
    (A : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀) (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†)))
    β†’ GlueOutput A T e

  has-strictly-coherent-glue : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
  has-strictly-coherent-glue =
    (A : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀) (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†)))
    β†’ GlueData A T e

  -- The strong Glue structure (Definition 5.2) demands contractibility of
  -- GlueData as a fibrant type (inner `is-contr` of its fibrant match).  Since
  -- the fibrancy of GlueData is established in `Extension.GlueDataFibrant`
  -- (which imports this module), the definition `has-strong-glue-structure`
  -- and Lemma 5.13(1) (`strong-to-strict`) live there.

  -- A homotopy coherent Glue structure for (i, 𝓀).
  has-homotopy-coherent-glue : UUᡉ (β„“Ο† βŠ” β„“Ξ¨ βŠ” lsuc 𝓀)
  has-homotopy-coherent-glue =
    (A : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀) (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†)))
    β†’ Σᡉ (GlueOutput A T e) (is-homotopy-coherent A T e)

  -- Unfolding of coerce-e: its underlying map is e's underlying map precomposed
  -- with the coercion idtoeqv(ΞΉ Ξ²_Ο†).  Proved by exo-J on the boundary Ξ², at
  -- reflᡉ the transport is the identity and ΞΉ Ξ²_Ο† is refl.  This is the
  -- `idtoeqv(ΞΉ Ξ²) ~ c_Ξ²` step of Lemma 5.13(3).
  coerce-e-und : (A : Ξ¨ β†’ UU 𝓀) (G : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀)
                 (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†)))
                 (Ξ² : (Ξ» Ο† β†’ G (i Ο†)) =ᡉ T) (Ο† : Ξ¦) (x : G (i Ο†))
               β†’ Id (pr1 (ic (coerce-e A T e G Ξ² Ο†)) x)
                    (pr1 (ic (e Ο†)) (pr1 (idtoeqv (ΞΉ-fun (Ξ» Ο†' β†’ G (i Ο†')) T Ξ² Ο†)) x))
  coerce-e-und A G .(Ξ» Ο†' β†’ G (i Ο†')) e reflᡉ Ο† x = refl

  -- The universal glue-data family W ψ = Ξ£(X:𝓀). X ≃ A ψ  (Lemma 5.1).
  W : (A : Ξ¨ β†’ UU 𝓀) β†’ Ξ¨ β†’ UU (lsuc 𝓀)
  W A ψ = Ξ£ (UU 𝓀) (Ξ» X β†’ X ≃ A ψ)

  -- Boundary correspondence, forward: the pair (Ξ², coherence) of a Glue datum
  -- gives the strict boundary of the corresponding W-section.  By exo-J on Ξ².
  bdry-pt : (A G : Ξ¨ β†’ UU 𝓀) (T : Ξ¦ β†’ UU 𝓀) (e : (Ο† : Ξ¦) β†’ C (T Ο† ≃ A (i Ο†)))
            (u : (ψ : Ξ¨) β†’ C (G ψ ≃ A ψ)) (Ξ² : (Ξ» Ο† β†’ G (i Ο†)) =ᡉ T)
            (cc : (Ο† : Ξ¦) β†’ u (i Ο†) =ᡉ coerce-e A T e G Ξ² Ο†) (Ο† : Ξ¦)
          β†’ c {A = W A (i Ο†)} (G (i Ο†) , ic (u (i Ο†))) =ᡉ c {A = W A (i Ο†)} (T Ο† , ic (e Ο†))
  bdry-pt A G .(Ξ» Ο†' β†’ G (i Ο†')) e u reflᡉ cc Ο† =
    exo-ap (Ξ» (q : C (G (i Ο†) ≃ A (i Ο†))) β†’ c {A = W A (i Ο†)} (G (i Ο†) , ic q)) (cc Ο†)

  -- Boundary correspondence, backward: the strict boundary p of a W-section
  -- gives the coherence of the corresponding Glue datum.  By exo-J on p.
  bdry-pt-inv : (A : Ξ¨ β†’ UU 𝓀) (w : (ψ : Ξ¨) β†’ C (W A ψ))
                (wβ‚€ : (Ο† : Ξ¦) β†’ C (W A (i Ο†)))
                (p : (Ξ» Ο† β†’ w (i Ο†)) =ᡉ wβ‚€) (Ο† : Ξ¦)
              β†’ c (pr2 (ic (w (i Ο†))))
                =ᡉ coerce-e A (Ξ» Ο†' β†’ pr1 (ic (wβ‚€ Ο†'))) (Ξ» Ο†' β†’ c (pr2 (ic (wβ‚€ Ο†'))))
                            (Ξ» ψ β†’ pr1 (ic (w ψ)))
                            (exo-ap (Ξ» v Ο†' β†’ pr1 (ic (v Ο†'))) p) Ο†
  bdry-pt-inv A w .(Ξ» Ο†' β†’ w (i Ο†')) reflᡉ Ο† = reflᡉ