Home

関数

module foundations.function where
Imports 
open import foundations.universe

関数の合成と恒等関数を定義する。

private variable
  ℓ : Level
  A B C : Type ℓ

infix 35 _∘_
_∘_ : (B → C) → (A → B) → A → C
g ∘ f = λ x → g (f x)

idFunction : ∀ (A : Type ℓ) → A → A
idFunction _ x = x