Precomposition of functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-01-14.

module foundation-core.precomposition-functions where
open import foundation.universe-levels

open import foundation-core.function-types


Given a function f : A → B and a type X, the precomposition function by f

  - ∘ f : (B → X) → (A → X)

is defined by λ h x → h (f x).


The precomposition operation on ordinary functions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) (C : UU l3)

  precomp : (B  C)  (A  C)
  precomp = _∘ f

Recent changes