Home

依存和型の要素の同一視

module foundations.sigma-type-identity where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.transport
open import foundations.bi-invertible-map
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.function
open import foundations.homotopy

private variable
  ℓ : Level
  A : Type ℓ
  B : A → Type ℓ

module _ {v w : Σ A B} where
  fromΣId : v ＝ w
    → Σ[ q ∈ fst v ＝ fst w ] (subst B q (snd v) ＝ snd w)
  fromΣId refl = refl , refl

この関数fromΣIdは同値である：

  ΣId : biinv fromΣId
  ΣId = QuasiInv⇒biinv (record
    { g = λ {(refl , refl) → refl}
    ; linv = λ {refl → refl}
    ; rinv = λ {(refl , refl) → refl}
    })

  toΣId : Σ[ q ∈ fst v ＝ fst w ] (subst B q (snd v) ＝ snd w)
    → v ＝ w
  toΣId = ΣId .fst .fst