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

--------------------------------------------------------------------------------
-- Theorem 5.15, with all five nodes and all five cyclic implications.
--
--   (1) 𝓤 is univalent;
--   (2) every full 2LTT cofibration has contractible Glue data;
--   (3) the boundary cofibration i∂ has contractible Glue data;
--   (4) i∂ has a strictly coherent Glue structure;
--   (5) (I, 0, 1, 𝓤) has a weak Glue structure.
--
-- The implications use an explicit witness of node (1).  No ambient
-- univalence constant is used.  Node (2) is the universe-polymorphic scheme
-- `AllStrongGlue`, which lives in SSetω because it quantifies over levels.
-- `ExactPathInterval` packages the theorem for the full PathInterval record.
-- The FibrantInterval and GeneralInterval modules retain useful auxiliary
-- variants, including fixed-level versions of node (2).
--------------------------------------------------------------------------------

module Extension.GlueSandwichFull where

open import Extension.Prelude
open import Extension.CofibFibration using (is-cofib)
open import Extension.RelFunext using (satisfies-rel-funext ; is-cofib-2LTT)
open import Extension.Univalence using (Univalence)
open import Extension.GlueStructure
  using (has-strictly-coherent-glue ; has-homotopy-coherent-glue ;
         strict-coh-to-homotopy-coh)
open import Extension.GlueDataFibrant
  using (has-strong-glue-structure ; strong-to-strict)
open import Extension.GlueRules using (WeakGlue)
open import Extension.GlueSandwich using (ua-strong-glue)
open import Extension.GlueStrengthChain3 using (strength-chain-3)
open import Extension.WeakGlueUAFibrant using (fibrant-weak-glue-implies-ua)
open import Extension.CoercionLaws
  using (PathStructure ; general-weak-glue-implies-ua)
import Extension.Conservativity as PathIntervalDef
open import Extension.GlueSandwichComplete using () renaming (i∂ to i∂-fib)
open import Extension.GlueSandwichGeneral using () renaming (i∂ to i∂-path)

private
  variable
    ℓI 𝓤' : Level

--------------------------------------------------------------------------------
-- The paper's implication (1) to (2) in full generality, at arbitrary shape
-- levels.  Its univalence witness and full cofibration witness are explicit.
-- The result cannot be placed in a fixed UUᵉ because it quantifies over Level.
--------------------------------------------------------------------------------

strong-glue-any-cofibration :
    {ℓΦ ℓΨ : Level} (𝓤 : Level) {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (U : Univalence 𝓤)
    (c2 : is-cofib-2LTT i (lsuc 𝓤))
  → has-strong-glue-structure i 𝓤 (pr1ᵉ c2)
strong-glue-any-cofibration 𝓤 U c2 = ua-strong-glue U (pr1ᵉ c2) (pr2ᵉ c2)

-- The paper's second node is a universe-polymorphic scheme.  It therefore
-- lives in the large outer universe rather than in one fixed UUᵉ level.
AllStrongGlue : (𝓤 : Level) → SSetω
AllStrongGlue 𝓤 =
  {ℓΦ ℓΨ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} →
  (c2 : is-cofib-2LTT i (lsuc 𝓤)) →
  has-strong-glue-structure i 𝓤 (pr1ᵉ c2)

--------------------------------------------------------------------------------
-- Variant A: fibrant interval  I = C 𝕀,  0 = c a₀,  1 = c a₁,  with a segment
-- seg : a₀ = a₁  (the hypotheses of `GlueSandwichComplete`).
--------------------------------------------------------------------------------

module FibrantInterval
         (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁)
         (cof  : is-cofib (i∂-fib 𝕀 a₀ a₁) (lsuc 𝓤))
         (triv : satisfies-rel-funext cof)
       where

  -- (1)  𝓤 is univalent.
  Cond1 : UU (lsuc 𝓤)
  Cond1 = (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})

  -- (2)  every full 2LTT cofibration (between exo-types at the level of i∂)
  --      carries a strong Glue structure.
  Cond2 : UUᵉ (lsuc (ℓI ⊔ lsuc 𝓤))
  Cond2 = {Φ Ψ : UUᵉ ℓI} (i : Φ → Ψ) (c2 : is-cofib-2LTT i (lsuc 𝓤))
        → has-strong-glue-structure i 𝓤 (pr1ᵉ c2)

  -- (3)  (i∂, 𝓤) has a strong Glue structure.
  Cond3 : UUᵉ (ℓI ⊔ lsuc 𝓤)
  Cond3 = has-strong-glue-structure (i∂-fib 𝕀 a₀ a₁) 𝓤 cof

  -- (4)  the paper's strictly coherent Glue structure for (i∂, 𝓤).
  Cond4 : UUᵉ (ℓI ⊔ lsuc 𝓤)
  Cond4 = has-strictly-coherent-glue (i∂-fib 𝕀 a₀ a₁) 𝓤

  -- (5)  weak Glue structure for (I, 0, 1, 𝓤).
  Cond5 : UUᵉ (ℓI ⊔ lsuc 𝓤)
  Cond5 = WeakGlue (C 𝕀) (c a₀) (c a₁) 𝓤

  -- (1)⇒(2): Theorem 5.4.
  1⇒2 : Cond1 → Cond2
  1⇒2 U i c2 = ua-strong-glue U (pr1ᵉ c2) (pr2ᵉ c2)

  -- (2)⇒(3): instantiate at i∂, a full 2LTT cofibration by hypothesis.
  2⇒3 : Cond2 → Cond3
  2⇒3 s2 = s2 (i∂-fib 𝕀 a₀ a₁) (cof ,ᵉ triv)

  -- (3)⇒(4): Lemma 5.13(1)+(2), extract the centre (a strictly
  -- coherent output) and coerce its strict coherence to a path.
  3⇒4 : Cond3 → Cond4
  3⇒4 = strong-to-strict (i∂-fib 𝕀 a₀ a₁) 𝓤 cof

  -- (4)⇒(5): Lemma 5.13(3).
  4⇒5 : Cond4 → Cond5
  4⇒5 scg = strength-chain-3 (C 𝕀) (i∂-fib 𝕀 a₀ a₁) 𝓤 hcg
    where
    hcg : has-homotopy-coherent-glue (i∂-fib 𝕀 a₀ a₁) 𝓤
    hcg A T e =
      pr1ᵉ gd ,ᵉ
      strict-coh-to-homotopy-coh (i∂-fib 𝕀 a₀ a₁) 𝓤 A T e (pr1ᵉ gd) (pr2ᵉ gd)
      where
      gd = scg A T e

  -- (5)⇒(1): Theorem 5.14 (fibrant-interval form).
  5⇒1 : Cond5 → Cond1
  5⇒1 = fibrant-weak-glue-implies-ua 𝕀 a₀ a₁ 𝓤 seg

  -- Theorem 5.15, the complete five-node cycle: all five conditions are
  -- equivalent.
  glue-sandwich-full :
       (Cond1 → Cond2)
    ×ᵉ ((Cond2 → Cond3)
    ×ᵉ ((Cond3 → Cond4)
    ×ᵉ ((Cond4 → Cond5)
    ×ᵉ  (Cond5 → Cond1))))
  glue-sandwich-full = 1⇒2 ,ᵉ (2⇒3 ,ᵉ (3⇒4 ,ᵉ (4⇒5 ,ᵉ 5⇒1)))

  -- Exact paper statement.  Node (2) quantifies over arbitrary universe
  -- levels and hence the package lives in SSetω.
  record ExactFiveNodeCycle : SSetω where
    field
      univalence-to-all : Cond1 → AllStrongGlue 𝓤
      all-to-boundary : AllStrongGlue 𝓤 → Cond3
      boundary-to-structure : Cond3 → Cond4
      structure-to-weak : Cond4 → Cond5
      weak-to-univalence : Cond5 → Cond1

  exact-five-node-cycle : ExactFiveNodeCycle
  exact-five-node-cycle = record
    { univalence-to-all = λ U {ℓΦ} {ℓΨ} {Φ} {Ψ} {i} c2 →
        strong-glue-any-cofibration 𝓤 {Φ = Φ} {Ψ = Ψ} {i = i} U c2
    ; all-to-boundary = λ all →
        all (cof ,ᵉ triv)
    ; boundary-to-structure = 3⇒4
    ; structure-to-weak = 4⇒5
    ; weak-to-univalence = 5⇒1
    }

--------------------------------------------------------------------------------
-- Variant B: general (not necessarily fibrant) path interval, presented by a
-- `PathStructure` (the hypotheses of `GlueSandwichGeneral`).
--------------------------------------------------------------------------------

module GeneralInterval
         (P : PathStructure ℓI 𝓤')
         (cof  : is-cofib (i∂-path P) (lsuc 𝓤'))
         (triv : satisfies-rel-funext cof)
       where

  Cond1 : UU (lsuc 𝓤')
  Cond1 = (A B : UU 𝓤') → isEquiv (idtoeqv {A = A} {B = B})

  Cond2 : UUᵉ (lsuc (ℓI ⊔ lsuc 𝓤'))
  Cond2 = {Φ Ψ : UUᵉ ℓI} (i : Φ → Ψ) (c2 : is-cofib-2LTT i (lsuc 𝓤'))
        → has-strong-glue-structure i 𝓤' (pr1ᵉ c2)

  Cond3 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond3 = has-strong-glue-structure (i∂-path P) 𝓤' cof

  Cond4 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond4 = has-strictly-coherent-glue (i∂-path P) 𝓤'

  Cond5 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond5 = WeakGlue (PathStructure.I P) (PathStructure.0I P) (PathStructure.1I P) 𝓤'

  1⇒2 : Cond1 → Cond2
  1⇒2 U i c2 = ua-strong-glue U (pr1ᵉ c2) (pr2ᵉ c2)

  2⇒3 : Cond2 → Cond3
  2⇒3 s2 = s2 (i∂-path P) (cof ,ᵉ triv)

  3⇒4 : Cond3 → Cond4
  3⇒4 = strong-to-strict (i∂-path P) 𝓤' cof

  4⇒5 : Cond4 → Cond5
  4⇒5 scg = strength-chain-3 (PathStructure.I P) (i∂-path P) 𝓤' hcg
    where
    hcg : has-homotopy-coherent-glue (i∂-path P) 𝓤'
    hcg A T e =
      pr1ᵉ gd ,ᵉ
      strict-coh-to-homotopy-coh (i∂-path P) 𝓤' A T e (pr1ᵉ gd) (pr2ᵉ gd)
      where
      gd = scg A T e

  5⇒1 : Cond5 → Cond1
  5⇒1 = general-weak-glue-implies-ua P

  glue-sandwich-full :
       (Cond1 → Cond2)
    ×ᵉ ((Cond2 → Cond3)
    ×ᵉ ((Cond3 → Cond4)
    ×ᵉ ((Cond4 → Cond5)
    ×ᵉ  (Cond5 → Cond1))))
  glue-sandwich-full = 1⇒2 ,ᵉ (2⇒3 ,ᵉ (3⇒4 ,ᵉ (4⇒5 ,ᵉ 5⇒1)))

  record ExactFiveNodeCycle : SSetω where
    field
      univalence-to-all : Cond1 → AllStrongGlue 𝓤'
      all-to-boundary : AllStrongGlue 𝓤' → Cond3
      boundary-to-structure : Cond3 → Cond4
      structure-to-weak : Cond4 → Cond5
      weak-to-univalence : Cond5 → Cond1

  exact-five-node-cycle : ExactFiveNodeCycle
  exact-five-node-cycle = record
    { univalence-to-all = λ U {ℓΦ} {ℓΨ} {Φ} {Ψ} {i} c2 →
        strong-glue-any-cofibration 𝓤' {Φ = Φ} {Ψ = Ψ} {i = i} U c2
    ; all-to-boundary = λ all →
        all (cof ,ᵉ triv)
    ; boundary-to-structure = 3⇒4
    ; structure-to-weak = 4⇒5
    ; weak-to-univalence = 5⇒1
    }

--------------------------------------------------------------------------------
-- The exact statement for the paper's PathInterval record.
--------------------------------------------------------------------------------

module ExactPathInterval
    (𝕀 : PathIntervalDef.PathInterval ℓI (lsuc 𝓤')) where

  private
    c2 = PathIntervalDef.i∂-cofib 𝕀
    cof = pr1ᵉ c2
    triv = pr2ᵉ c2
    i∂ = PathIntervalDef.i∂ 𝕀
    P = PathIntervalDef.PathInterval-to-PathStructure 𝕀

  Cond1 : UU (lsuc 𝓤')
  Cond1 = Univalence 𝓤'

  Cond3 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond3 = has-strong-glue-structure i∂ 𝓤' cof

  Cond4 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond4 = has-strictly-coherent-glue i∂ 𝓤'

  Cond5 : UUᵉ (ℓI ⊔ lsuc 𝓤')
  Cond5 = WeakGlue (PathIntervalDef.I 𝕀)
    (PathIntervalDef.0I 𝕀) (PathIntervalDef.1I 𝕀) 𝓤'

  3⇒4 : Cond3 → Cond4
  3⇒4 = strong-to-strict i∂ 𝓤' cof

  4⇒5 : Cond4 → Cond5
  4⇒5 scg = strength-chain-3 (PathIntervalDef.I 𝕀) i∂ 𝓤' hcg
    where
    hcg : has-homotopy-coherent-glue i∂ 𝓤'
    hcg A T e =
      pr1ᵉ gd ,ᵉ
      strict-coh-to-homotopy-coh i∂ 𝓤' A T e (pr1ᵉ gd) (pr2ᵉ gd)
      where
      gd = scg A T e

  5⇒1 : Cond5 → Cond1
  5⇒1 = general-weak-glue-implies-ua P

  record ExactFiveNodeCycle : SSetω where
    field
      univalence-to-all : Cond1 → AllStrongGlue 𝓤'
      all-to-boundary : AllStrongGlue 𝓤' → Cond3
      boundary-to-structure : Cond3 → Cond4
      structure-to-weak : Cond4 → Cond5
      weak-to-univalence : Cond5 → Cond1

  exact-five-node-cycle : ExactFiveNodeCycle
  exact-five-node-cycle = record
    { univalence-to-all = λ U {ℓΦ} {ℓΨ} {Φ} {Ψ} {i} c2' →
        strong-glue-any-cofibration 𝓤' {Φ = Φ} {Ψ = Ψ} {i = i} U c2'
    ; all-to-boundary = λ all → all c2
    ; boundary-to-structure = 3⇒4
    ; structure-to-weak = 4⇒5
    ; weak-to-univalence = 5⇒1
    }