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

--------------------------------------------------------------------------------
-- Internal content of the comparison in Section 6, using the exact axiom
-- schemes from Definition 6.2.
--------------------------------------------------------------------------------

module Extension.TheoryComparison where

open import Extension.Prelude
open import Extension.Univalence using (Univalence)
open import Extension.Conservativity
  using (Axiom-glue ; PathInterval ; I ; i∂ ; 0I ; 1I ; i∂-cofib ;
         PathInterval-to-PathStructure)
open import Extension.GlueDataFibrant using (strong-to-strict)
open import Extension.GlueSandwich using (ua-strong-glue)
open import Extension.GlueStructure
  using (has-strictly-coherent-glue ; has-homotopy-coherent-glue ;
         strict-coh-to-homotopy-coh)
open import Extension.GlueRules using (WeakGlue)
open import Extension.GlueStrengthChain3 using (strength-chain-3)
open import Extension.CoercionLaws using (general-weak-glue-implies-ua)
open import Extension.RelFunext using (is-cofib-2LTT)

private
  variable
    ℓΦ ℓΨ ℓI 𝓤 : Level

-- (ua) implies the exact (glue) scheme.  The domain-cofibrancy hypothesis in
-- Axiom-glue is not needed by the stronger Theorem 5.4.
univalence-implies-glue :
  {ℓΦ ℓΨ 𝓤 : Level} →
  Univalence 𝓤 → Axiom-glue ℓΦ ℓΨ 𝓤
univalence-implies-glue {ℓΦ = ℓΦ} {ℓΨ = ℓΨ} {𝓤 = 𝓤}
  U Φ Ψ i c2 _ =
  strong-to-strict i 𝓤 (pr1ᵉ c2)
    (ua-strong-glue U (pr1ᵉ c2) (pr2ᵉ c2))

-- (int) and the exact (glue) scheme imply (ua).  The two-point boundary is
-- cofibrant because it is a coproduct of two cofibrant unit types.
interval-and-glue-imply-univalence :
  {ℓI 𝓤 : Level} →
  PathInterval ℓI (lsuc 𝓤) →
  Axiom-glue ℓI ℓI 𝓤 →
  Univalence 𝓤
interval-and-glue-imply-univalence {ℓI = ℓI} {𝓤 = 𝓤} 𝕀 glue =
  general-weak-glue-implies-ua (PathInterval-to-PathStructure 𝕀) weak
  where
  cof∂ : isCofibrant (⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) (lsuc 𝓤)
  cof∂ = +ᵉ-preserve-Cofibrant
    (⊤ᵉ-is-cofibrant (lsuc 𝓤)) (⊤ᵉ-is-cofibrant (lsuc 𝓤))

  strict : has-strictly-coherent-glue (i∂ 𝕀) 𝓤
  strict = glue (⊤ᵉ +ᵉ ⊤ᵉ) (I 𝕀) (i∂ 𝕀) (i∂-cofib 𝕀) cof∂

  homotopy : has-homotopy-coherent-glue (i∂ 𝕀) 𝓤
  homotopy A T e =
    pr1ᵉ gd ,ᵉ
    strict-coh-to-homotopy-coh (i∂ 𝕀) 𝓤 A T e (pr1ᵉ gd) (pr2ᵉ gd)
    where
    gd = strict A T e

  weak : WeakGlue (I 𝕀) (0I 𝕀) (1I 𝕀) 𝓤
  weak = strength-chain-3 (I 𝕀) (i∂ 𝕀) 𝓤 homotopy