This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Postcomposition of functions

module foundation-core.postcomposition-functions where

Imports

open import foundation.universe-levels

open import foundation-core.postcomposition-dependent-functions

Idea

Given a map f : X → Y and a type A, the postcomposition function^¶

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

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

module _
  {l1 l2 l3 : Level} (A : UU l1) {X : UU l2} {Y : UU l3}
  where

  postcomp : (X → Y) → (A → X) → (A → Y)
  postcomp f = postcomp-Π A f