module foundations.happly where
open import foundations.universe open import foundations.identity-type open import foundations.homotopy open import foundations.functions-are-functors
2つの関数を同一視できるなら、それらの間のホモトピーを選択することができる。
private variable ℓ : Level A : Type ℓ B : A → Type ℓ f g : (a : A) → B a happly : f ＝ g → f ~ g happly p x = ap (λ w → w x) p