Home

ファイブレーション

module foundations.fibration where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.transport

型族B : A → Type ℓについて、Σ A Bをtotal spaceと見なすことができる。そして、底空間Aへの射影fstはファイブレーションとなる。

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

pathLiftingProperty : ∀ (p : x ＝ y) (v : B x)
  → Id (Σ A B) (x , v) (y , subst B p v)
pathLiftingProperty refl _ = refl