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

--------------------------------------------------------------------------------
-- Theorem 5.15, the complete cycle, for a general path interval.
--
-- For a path interval presented by a `PathStructure` (the interface of
-- Lemma 5.8; not necessarily fibrant), with boundary inclusion i∂ a
-- full 2LTT cofibration, the fibration half `cof` plus the trivial half
-- `triv` (relative funext); no cofibrancy of I or ∂I is assumed, conditions
-- (1) univalence, (4) a homotopy coherent Glue structure for (i∂, 𝓤), and (5)
-- a weak Glue structure for (I, 0, 1, 𝓤) are inter-derivable:
--
--   1⇒4  `GlueSandwich.ua-homotopy-coherent-glue`;
--   4⇒5  `GlueStrengthChain3.strength-chain-3`;
--   5⇒1  `CoercionLaws.general-weak-glue-implies-ua` (Theorem 5.14
--        with the coercion laws derived from the path presentation).
--
-- Unlike `GlueSandwichComplete`, this does not assume the interval is fibrant:
-- the coercion laws come from the path presentation (`PathStructure`) rather
-- than from a segment transport.
--------------------------------------------------------------------------------

module Extension.GlueSandwichGeneral where

open import Extension.Prelude
open import Extension.CofibFibration using (is-cofib)
open import Extension.RelFunext using (satisfies-rel-funext)
open import Extension.GlueStructure using (has-homotopy-coherent-glue)
open import Extension.GlueRules using (WeakGlue)
open import Extension.GlueSandwich using (ua-homotopy-coherent-glue)
open import Extension.GlueStrengthChain3 using (strength-chain-3)
open import Extension.CoercionLaws using (PathStructure ; general-weak-glue-implies-ua)

private
  variable
    ℓI 𝓤 : Level

-- Boundary inclusion of the path interval: ∂I = ⊤ + ⊤ → I, hitting the endpoints.
i∂ : (P : PathStructure ℓI 𝓤) → (⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) → PathStructure.I P
i∂ P (inlᵉ _) = PathStructure.0I P
i∂ P (inrᵉ _) = PathStructure.1I P

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

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

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

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

  1⇒4 : Cond1 → Cond4
  1⇒4 U = ua-homotopy-coherent-glue U cof triv

  4⇒5 : Cond4 → Cond5
  4⇒5 hcg = strength-chain-3 (PathStructure.I P) (i∂ P) 𝓤 hcg

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

  -- The complete cycle for a general path interval.
  glue-sandwich : (Cond1 → Cond4) ×ᵉ ((Cond4 → Cond5) ×ᵉ (Cond5 → Cond1))
  glue-sandwich = 1⇒4 ,ᵉ (4⇒5 ,ᵉ 5⇒1)