{-# OPTIONS --without-K #-}
module hott.univalence where

open import level using (lsuc)
open import sum using (_,_ ; proj₁)
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.isomorphism.core using (_≅_ ; module _≅_)
open import hott.equivalence.core

-- mapping from equality to function
coerce :  {i} {X Y : Set i}  X  Y  X  Y
coerce refl = id

coerce-equiv :  {i} {X Y : Set i}  (p : X  Y)  weak-equiv (coerce p)
coerce-equiv refl x = (x , refl) , λ { (.x , refl)  refl }

coerce-hom :  {i} {X Y Z : Set i}
            (p : X  Y)(q : Y  Z)
            coerce (p · q)  coerce q  coerce p
coerce-hom refl q = refl

-- mapping from propositional equality to weak equivalence
≡⇒≈ :  {i} {X Y : Set i}  X  Y  X  Y
≡⇒≈ p = coerce p , coerce-equiv p

Univalence :  i  Set (lsuc i)
Univalence i = {X Y : Set i}  weak-equiv $ ≡⇒≈ {X = X} {Y = Y}

postulate univalence :  {i}  Univalence i

module _ {i} {X Y : Set i} where
  uni-equiv : (X  Y)  (X  Y)
  uni-equiv = ≡⇒≈ , univalence

  uni-iso : (X  Y)  (X  Y)
  uni-iso = ≈⇒≅ uni-equiv
  open _≅_ uni-iso public using ()
    renaming (from to ≈⇒≡)

  uni-coherence : (f : X  Y)  coerce (≈⇒≡ f)  proj₁ f
  uni-coherence f = begin
      coerce (≈⇒≡ f)
    ≡⟨ refl 
      proj₁ (≡⇒≈ (≈⇒≡ f))
    ≡⟨ ap proj₁ (iso₂ f) 
      proj₁ f
    
    where
      open ≡-Reasoning
      open _≅_ uni-iso using (iso₂)