{-# 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.weak-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

private
  module Properties {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₂)

open Properties public