第2成分の型が可縮であるような依存和型

module foundations.sigma-type-snd-contr where

open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.contractible-type
open import foundations.bi-invertible-map
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.function
open import foundations.homotopy
open import foundations.sigma-type-identity

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

module _ (f : ∀ (a : A) → isContr (B a)) where
  ΣSndContr : biinv {A = Σ A B} fst
  ΣSndContr = QuasiInv⇒biinv record
    { g = λ x → x , f x .fst
    ; linv = λ {(a , b) → toΣId (refl , f a .snd b)}
    ; rinv = λ _ → refl
    }