Home

依存マップ

module foundations.dependent-map where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.transport
open import foundations.groupoid-laws
open import foundations.functions-are-functors

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

apd : ∀ {x y : A}
  → (f : (a : A) → B a)
  → (p : x ＝ y)
  → subst B p (f x) ＝ f y
apd _ refl = refl

apdとapは次のように関連付けられる。

apd＝substConst∙ap : ∀ {x y : A}
  → (f : A → C)
  → (p : x ＝ y)
  → apd f p ＝ substConst p (f x) ∙ ap f p
apd＝substConst∙ap _ refl = sym (lunitId refl)