{-# OPTIONS --without-K #-}

module hott.equivalence.properties where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.isomorphism
open import function.extensionality
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.univalence
open import hott.level

sym≈ : ∀ {i j}{X : Set i}{Y : Set j}
     → X ≈ Y → Y ≈ X
sym≈ = ≅'⇒≈ ∘ sym≅' ∘ ≈⇒≅'

-- being a weak equivalence is propositional
we-h1 : ∀ {i j}{X : Set i}{Y : Set j}
      → (f : X → Y)
      → h  (weak-equiv f)
we-h1 f = Π-level λ _ → contr-h1 _

apply≈-inj : ∀ {i j}{X : Set i}{Y : Set j}
           → injective (apply≈ {X = X}{Y = Y})
apply≈-inj {x = (f , w)}{.f , w'} refl =
  unapΣ (refl , h1⇒prop (we-h1 f) w w')

abstract
  univ-sym≈ : ∀ {i}{X Y : Set i}
            → (w : X ≈ Y)
            → sym (≈⇒≡ w)
            ≡ ≈⇒≡ (sym≈ w)
  univ-sym≈ {i}{X}{Y} w = inverse-unique p q lem-inv
    where
      p : X ≡ Y
      p = ≈⇒≡ w

      q : Y ≡ X
      q = ≈⇒≡ (sym≈ w)

      p-β : coerce p ≡ apply≈ w
      p-β = uni-coherence w

      q-β : coerce q ≡ invert≈ w
      q-β = uni-coherence (sym≈ w)

      lem : coerce (p · q) ≡ coerce refl
      lem = coerce-hom p q
          · (ap (λ h → coerce q ∘ h) p-β
          · ap (λ h → h ∘ apply≈ w) q-β
          · funext (_≅_.iso₁ (≈⇒≅ w)))

      lem-inv : p · q ≡ refl
      lem-inv = iso⇒inj uni-iso (apply≈-inj lem)