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

--------------------------------------------------------------------------------
-- Theorem 5.15, the complete cycle, for a fibrant interval.
--
-- For a fibrant interval I = C 𝕀 with segment seg : aβ‚€ = a₁ and 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,
-- the following are inter-derivable:
--
--   (1)  𝓀 is univalent  [Cond1];
--   (4)  a homotopy coherent Glue structure for (iβˆ‚, 𝓀)  [Cond4];
--   (5)  a weak Glue structure for (I, 0, 1, 𝓀)  [Cond5].
--
-- with the cyclic implications (1)β‡’(4)β‡’(5)β‡’(1):
--   1β‡’4  `GlueSandwich.ua-homotopy-coherent-glue`, (1)β‡’(2)β‡’(3)β‡’(4): univalence
--        gives the strong Glue data (Theorem 5.4 via
--        Lemma 5.1), whose centre is a strictly coherent output,
--        coerced to homotopy coherence (Lemma 5.13(1),(2));
--   4β‡’5  `GlueStrengthChain3.strength-chain-3` (Lemma 5.13(3));
--   5β‡’1  `WeakGlueUAFibrant.fibrant-weak-glue-implies-ua` (Theorem 5.14).
--
-- The intermediate strong-Glue conditions are compressed into 1β‡’4.  That map
-- consumes its Cond1 argument explicitly; 5β‡’1 constructs a new univalence
-- witness from weak Glue.
--------------------------------------------------------------------------------

module Extension.GlueSandwichComplete 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.WeakGlueUAFibrant using (fibrant-weak-glue-implies-ua)

private
  variable
    β„“I : Level

-- Boundary inclusion of a fibrant interval  I = C 𝕀,  0 = c aβ‚€, 1 = c a₁.
iβˆ‚ : (𝕀 : UU β„“I) (aβ‚€ a₁ : 𝕀) β†’ (βŠ€α΅‰ {β„“I} +ᡉ βŠ€α΅‰ {β„“I}) β†’ C 𝕀
iβˆ‚ 𝕀 aβ‚€ a₁ (inlᡉ _) = c aβ‚€
iβˆ‚ 𝕀 aβ‚€ a₁ (inrᡉ _) = c a₁

module _ (𝕀 : UU β„“I) (aβ‚€ a₁ : 𝕀) (𝓀 : Level) (seg : Id aβ‚€ a₁)
         (cof  : is-cofib (iβˆ‚ 𝕀 aβ‚€ a₁) (lsuc 𝓀))
         (triv : satisfies-rel-funext cof)
       where

  -- The three conditions.
  Cond1 : UU (lsuc 𝓀)
  Cond1 = (A B : UU 𝓀) β†’ isEquiv (idtoeqv {A = A} {B = B})

  Cond4 : UUᡉ (lsuc 𝓀 βŠ” β„“I)
  Cond4 = has-homotopy-coherent-glue (iβˆ‚ 𝕀 aβ‚€ a₁) 𝓀

  Cond5 : UUᡉ (β„“I βŠ” lsuc 𝓀)
  Cond5 = WeakGlue (C 𝕀) (c aβ‚€) (c a₁) 𝓀

  -- (1)β‡’(2)β‡’(3)β‡’(4).
  1β‡’4 : Cond1 β†’ Cond4
  1β‡’4 U = ua-homotopy-coherent-glue U cof triv

  -- (4)β‡’(5).
  4β‡’5 : Cond4 β†’ Cond5
  4β‡’5 hcg = strength-chain-3 (C 𝕀) (iβˆ‚ 𝕀 aβ‚€ a₁) 𝓀 hcg

  -- (5)β‡’(1).
  5β‡’1 : Cond5 β†’ Cond1
  5β‡’1 = fibrant-weak-glue-implies-ua 𝕀 aβ‚€ a₁ 𝓀 seg

  -- The complete cycle: the three conditions are equivalent.  In particular,
  -- univalence round-trips through the gluing conditions.
  glue-sandwich : (Cond1 β†’ Cond4) ×ᡉ ((Cond4 β†’ Cond5) ×ᡉ (Cond5 β†’ Cond1))
  glue-sandwich = 1β‡’4 ,ᡉ (4β‡’5 ,ᡉ 5β‡’1)