# Postcomposition of dependent functions

```agda
module foundation.postcomposition-dependent-functions where

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

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

Given a type `A` and a family of maps `f : {a : A} → X a → Y a`, the
{{#concept "postcomposition function" Disambiguation="of dependent functions by a family of maps" Agda=postcomp-Π}}
of dependent functions `(a : A) → X a` by the family of maps `f`

```text
  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](foundation-core.postcomposition-functions.md) in
the same way that
[precomposition of dependent functions](foundation-core.precomposition-dependent-functions.md)
generalizes
[precomposition of functions](foundation-core.precomposition-functions.md). If
`A` can vary while keeping `f` fixed, we have necessarily reduced to the case of
[postcomposition of functions](foundation-core.postcomposition-functions.md).

## 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](foundation.action-on-identifications-functions.md)
`ap (postcomp-Π A f)` fits in a
[commuting square](foundation-core.commuting-squares-of-maps.md)

```text
                   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

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

```agda
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-Π)
```