Home

型の同値性は同値関係である

module foundations.equivalence-is-equivalence-relation where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.bi-invertible-map
open import foundations.function
open import foundations.sigma-type
open import foundations.quasi-inverse
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.bi-invertible-map-to-quasi-inverse
open import foundations.homotopy
open import foundations.functions-are-functors
open import foundations.identity-type-reasoning

private variable
  ℓ : Level
  A B C : Type ℓ

biinvIdFunction : biinv (idFunction A)
biinvIdFunction = QuasiInv⇒biinv (record
  { g = idFunction _
  ; linv = λ _ → refl
  ; rinv = λ _ → refl
  })

refl≃ : A ≃ A
refl≃ = idFunction _ , biinvIdFunction

sym≃ : A ≃ B → B ≃ A
sym≃ (f , b) =
  g , QuasiInv⇒biinv (record { g = f ; linv = rinv ; rinv = linv })
  where
    open QuasiInv (biinv⇒QuasiInv b)

trans≃ : A ≃ B → B ≃ C → A ≃ C
trans≃ (f , b) (f′ , c) =
  f′ ∘ f , QuasiInv⇒biinv (record { g = q.g ∘ r.g ; linv = linv ; rinv = rinv })
  where
    module q = QuasiInv (biinv⇒QuasiInv b)
    module r = QuasiInv (biinv⇒QuasiInv c)

    linv : ∀ x → q.g (r.g (f′ (f x))) ＝ x
    linv x =
        q.g (r.g (f′ (f x)))
      ＝⟨ ap q.g (r.linv (f x)) ⟩
        q.g (f x)
      ＝⟨ q.linv x ⟩
        x
      ∎

    rinv : ∀ x → f′ (f (q.g (r.g x))) ＝ x
    rinv x =
        f′ (f (q.g (r.g x)))
      ＝⟨ ap f′ (q.rinv (r.g x)) ⟩
        f′ (r.g x)
      ＝⟨ r.rinv x ⟩
        x
      ∎