Home

ホモトピー

module foundations.homotopy where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.groupoid-laws

ホモトピーを定義する。

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

infix 20 _~_

_~_ : ∀ (f g : (a : A) → B a) → Type _
f ~ g = ∀ x → f x ＝ g x

ホモトピーは同値関係である。

private variable
  f g h : (a : A) → B a

reflHtpy : f ~ f
reflHtpy _ = refl

symHtpy : f ~ g → g ~ f
symHtpy H x = sym (H x)

transHtpy : f ~ g → g ~ h → f ~ h
transHtpy H I x = H x ∙ I x