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
open import foundation.universe-levels

open import foundation-core.function-types


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.


Postcomposition of dependent functions

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

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

Recent changes