Home

「第2成分の型が命題であるような依存和型」の要素の同一視

module foundations.sigma-type-identity-snd-prop where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.sigma-type-identity
open import foundations.sigma-type-snd-contr
open import foundations.proposition
open import foundations.transport
open import foundations.bi-invertible-map
open import foundations.equivalence-is-equivalence-relation
open import foundations.prop-id-contr

private variable ℓ ℓ′ : Level

module _ {A : Type ℓ} {B : A → Type ℓ′}
  (isPropB : ∀ a → isProp (B a))
  {v w : Σ A B} where
  ΣIdSndProp≃ : (v ＝ w) ≃ (fst v ＝ fst w)
  ΣIdSndProp≃ =
    trans≃
      (fromΣId , ΣId)
      (fst , ΣSndContr λ _ → isProp⇒isContrId (isPropB _))

  ΣIdSndProp : biinv (λ (p : v ＝ w) → fromΣId p .fst)
  ΣIdSndProp = ΣIdSndProp≃ .snd

  toΣIdSndProp : fst v ＝ fst w → v ＝ w
  toΣIdSndProp = sym≃ ΣIdSndProp≃ .fst