{-# 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₂)