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

--------------------------------------------------------------------------------
-- Remark 5.9 + Theorem 5.14, fully closed.
--
-- For a *fibrant* interval the path presentation collapses to a single segment
-- seg : 0 = 1, and the coercion laws of Lemma 5.8 become the standard
-- transport facts:
--   coe^G ≔ transport^G(seg),   path(G) ≔ ap_G(seg),
--   (c1) idtoeqv(ap_G p) ~ transport^G(p);
--   (c2) fibrewise maps commute with transport;
--   (c3) transport in a constant family is the identity.
-- Discharging the coercion interface of `Extension.WeakGlueUA` with these gives a
-- fully self-contained theorem: a weak Glue structure over a fibrant interval
-- implies univalence.
--
-- We present the fibrant interval as  I ≔ C 𝕀  for an inner 𝕀 : UU, with points
-- c a₀, c a₁ and segment seg : a₀ = a₁ (the inner identity of 𝕀).
--------------------------------------------------------------------------------

module Extension.WeakGlueUAFibrant where

open import Extension.Prelude
open import Extension.GlueRules using (WeakGlue)
open import Extension.CoercionLaws using (PathStructure)
open import Extension.WeakGlueUA using (weak-glue-implies-ua)

private
  variable
    ℓ 𝓤 : Level

-- (c1) idtoeqv of ap is transport.
idtoeqv-ap-tr : {A : UU ℓ} {a b : A} (F : A → UU 𝓤) (p : Id a b) (x : F a)
              → Id (pr1 (idtoeqv (ap F p)) x) (tr F p x)
idtoeqv-ap-tr F refl x = refl

-- (c2) fibrewise maps commute with transport.
tr-nat : {A : UU ℓ} {a b : A} (F H : A → UU 𝓤) (θ : (z : A) → F z → H z)
         (p : Id a b) (x : F a) → Id (θ b (tr F p x)) (tr H p (θ a x))
tr-nat F H θ refl x = refl

-- (c3) transport in a constant family is the identity.
tr-const : {A : UU ℓ} {a b : A} (Y : UU 𝓤) (p : Id a b) (x : Y)
         → Id (tr (λ _ → Y) p x) x
tr-const Y refl x = refl

-- A fibrant interval carries the standard line-to-identity structure obtained
-- by applying a line to its distinguished segment.  Degeneracy on constant
-- lines is not part of the interface: it is derived from naturality in
-- `Extension.CoercionLaws`.
fibrant-path-structure : {ℓI : Level} (𝕀 : UU ℓI) (a₀ a₁ : 𝕀)
                         (𝓤 : Level) (seg : Id a₀ a₁) → PathStructure ℓI 𝓤
fibrant-path-structure 𝕀 a₀ a₁ 𝓤 seg = record
  { I = C 𝕀
  ; 0I = c a₀
  ; 1I = c a₁
  ; path = λ g → ap (λ z → ic (g (c z))) seg
  ; path-nat = λ h g → ap-comp h (λ z → ic (g (c z))) seg
  }

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

  private
    I : UUᵉ ℓI
    I = C 𝕀
    0I 1I : I
    0I = c a₀
    1I = c a₁

    coeF : (G : I → UU 𝓤) → G 0I → G 1I
    coeF G = tr (λ z → G (c z)) seg

    pathF : (G : I → UU 𝓤) → Id (G 0I) (G 1I)
    pathF G = ap (λ z → G (c z)) seg

    c1F : (G : I → UU 𝓤) (x : G 0I) → Id (coeF G x) (pr1 (idtoeqv (pathF G)) x)
    c1F G x = (idtoeqv-ap-tr (λ z → G (c z)) seg x) ⁻¹

    c2F : (G H : I → UU 𝓤) (θ : (t : I) → G t → H t) (x : G 0I)
        → Id (θ 1I (coeF G x)) (coeF H (θ 0I x))
    c2F G H θ x = tr-nat (λ z → G (c z)) (λ z → H (c z)) (λ z → θ (c z)) seg x

    c3F : (Y : UU 𝓤) (x : Y) → Id (coeF (λ _ → Y) x) x
    c3F Y x = tr-const Y seg x

  -- The fully-closed theorem: weak glue over a fibrant interval ⇒ univalence.
  fibrant-weak-glue-implies-ua : WeakGlue I 0I 1I 𝓤
                               → (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})
  fibrant-weak-glue-implies-ua =
    weak-glue-implies-ua I 0I 1I 𝓤 coeF pathF c1F c2F c3F