{-# 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
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
≡⇒≈ : ∀ {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