Postcomposition of dependent functions

Content created by Fredrik Bakke.

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

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

open import foundation-core.function-types

Idea

Given a type A and a family of maps f : {a : A} → X a → Y a, the postcomposition function of dependent functions (a : A) → X a by the family of maps f

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

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

Note that, since the definition of the family of maps f depends on the base A, postcomposition of dependent functions does not generalize postcomposition of functions in the same way that precomposition of dependent functions generalizes precomposition of functions. If A can vary while keeping f fixed, we have necessarily reduced to the case of postcomposition of functions.

Definitions

Postcomposition of dependent functions

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

  postcomp-Π : ({a : A} → X a → Y a) → ((a : A) → X a) → ((a : A) → Y a)
  postcomp-Π f = f ∘_

Recent changes