# Postcomposition of dependent functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-14.

module foundation.postcomposition-dependent-functions where

open import foundation-core.postcomposition-dependent-functions public

Imports
open import foundation.action-on-identifications-functions
open import foundation.function-extensionality
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.function-types
open import foundation-core.identity-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.

## Properties

### The action on identifications of postcomposition by a family map

Consider a map f : {x : A} → B x → C x and two functions g h : (x : A) → B x. Then the action on identifications ap (postcomp-Π A f) fits in a commuting square

                   ap (postcomp-Π A f)
(g ＝ h) -------------------------> (f ∘ g ＝ f ∘ h)
|                                       |
htpy-eq |                                       | htpy-eq
∨                                       ∨
(g ~ h) --------------------------> (f ∘ g ~ f ∘ h).
f ·l_


Similarly, the action on identifications ap (postcomp-Π A f) fits in a commuting square

                    ap (postcomp-Π A f)
(g ＝ h) -------------------------> (f ∘ g ＝ f ∘ h)
∧                                       ∧
eq-htpy |                                       | eq-htpy
|                                       |
(g ~ h) --------------------------> (f ∘ g ~ f ∘ h).
f ·l_

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

compute-htpy-eq-ap-postcomp-Π :
coherence-square-maps
( ap (postcomp-Π A f) {x = g} {y = h})
( htpy-eq)
( htpy-eq)
( f ·l_)
compute-htpy-eq-ap-postcomp-Π refl = refl

compute-eq-htpy-ap-postcomp-Π :
coherence-square-maps
( f ·l_)
( eq-htpy)
( eq-htpy)
( ap (postcomp-Π A f))
compute-eq-htpy-ap-postcomp-Π =
vertical-inv-equiv-coherence-square-maps
( ap (postcomp-Π A f))
( equiv-funext)
( equiv-funext)
( f ·l_)
( compute-htpy-eq-ap-postcomp-Π)