Postcomposition of dependent functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-14.
Last modified on 2024-04-25.

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

Recent changes