Postcomposition of functions

Content created by Fredrik Bakke.

Created on 2024-01-14.
Last modified on 2024-03-20.

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

Definitions

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

Recent changes