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

Precomposition of functions

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

open import foundation-core.function-types

Idea

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).

Definitions

The precomposition operation on ordinary functions

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

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