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

--------------------------------------------------------------------------------
-- Theorem 5.15, the (4)⇒(5)⇒(1) fragment, for a fibrant interval.
--
-- For a fibrant interval  I = C 𝕀  with points c a₀, c a₁ and segment
-- seg : a₀ = a₁, the boundary inclusion i∂ : ∂I → I, and any universe 𝓤:
--
--     a homotopy coherent Glue structure for (i∂, 𝓤)  ⟹  𝓤 is univalent.
--
-- This composes the two pieces:
--   * Lemma 5.13(3)  (`GlueStrengthChain3.strength-chain-3`):
--       a homotopy coherent Glue structure yields a weak Glue structure;
--   * Theorem 5.14 for a fibrant interval
--       (`WeakGlueUAFibrant.fibrant-weak-glue-implies-ua`):
--       a weak Glue structure implies univalence.
-- Together with `UAStrongGlue.ua-implies-strong-glue` (the (1)⇒… direction) and
-- `GlueRules.ua-gives-weak-glue`, this closes the equivalence of univalence with
-- (homotopy-coherent / weak) gluing over a fibrant interval, modulo the encoding
-- Lemma 5.1 that identifies the strong Glue data with the extension
-- type (which links this to the strict-coherent form of the sandwich).
--------------------------------------------------------------------------------

module Extension.GlueSandwichFibrant where

open import Extension.Prelude
open import Extension.GlueStructure using (has-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

module _ (𝕀 : UU ℓI) (a₀ a₁ : 𝕀) (𝓤 : Level) (seg : Id a₀ a₁) where

  -- public: part of the statement of `htpy-coherent-glue-implies-ua`
  -- (referenced by the paper index src/index.agda)
  i∂ : (⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) → C 𝕀
  i∂ (inlᵉ _) = c a₀
  i∂ (inrᵉ _) = c a₁

  htpy-coherent-glue-implies-ua :
      has-homotopy-coherent-glue i∂ 𝓤
    → (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})
  htpy-coherent-glue-implies-ua hcg =
    fibrant-weak-glue-implies-ua 𝕀 a₀ a₁ 𝓤 seg
      (strength-chain-3 (C 𝕀) i∂ 𝓤 hcg)