Precomposition of functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-02-19.

module foundation.precomposition-functions where

open import foundation-core.precomposition-functions public
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.precomposition-dependent-functions
open import foundation.sections
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.commuting-triangles-of-maps
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.retractions

Idea

Given a function f : A → B and a type X, the precomposition function by f

  - ∘ f : (B → X) → (A → X)

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

The precomposition function was already defined in foundation-core.precomposition-functions. In this file we derive some further properties of the precomposition function.

Properties

Precomposition preserves homotopies

htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {f g : A  B} (H : f ~ g) (C : UU l3) 
  precomp f C ~ precomp g C
htpy-precomp H C h = eq-htpy (h ·l H)

compute-htpy-precomp-refl-htpy :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) (C : UU l3) 
  htpy-precomp (refl-htpy' f) C ~ refl-htpy
compute-htpy-precomp-refl-htpy f C h = eq-htpy-refl-htpy (h  f)

Precomposition preserves concatenation of homotopies

compute-concat-htpy-precomp :
  { l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  { f g h : A  B} (H : f ~ g) (K : g ~ h) (C : UU l3) 
  htpy-precomp (H ∙h K) C ~ htpy-precomp H C ∙h htpy-precomp K C
compute-concat-htpy-precomp H K C k =
  ( ap
    ( eq-htpy)
    ( eq-htpy (distributive-left-whisker-comp-concat k H K))) 
  ( eq-htpy-concat-htpy (k ·l H) (k ·l K))

If precomposition - ∘ f : (Y → X) → (X → X) has a section, then f has a retraction

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)
  where

  retraction-section-precomp-domain : section (precomp f X)  retraction f
  pr1 (retraction-section-precomp-domain s) =
    map-section (precomp f X) s id
  pr2 (retraction-section-precomp-domain s) =
    htpy-eq (is-section-map-section (precomp f X) s id)

Equivalences induce an equivalence from the type of homotopies between two maps to the type of homotopies between their precomposites

module _
  { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  where

  equiv-htpy-precomp-htpy :
    (f g : B  C) (e : A  B)  (f ~ g)  (f  map-equiv e ~ g  map-equiv e)
  equiv-htpy-precomp-htpy f g e =
    equiv-htpy-precomp-htpy-Π f g e

Computations of the fibers of precomp

The fiber of - ∘ f : (B → X) → (A → X) at g ∘ f : B → X is equivalent to the type of maps h : B → X equipped with a homotopy witnessing that the square

        f
    A -----> B
    |        |
  f |        | h
    V        V
    B -----> X
        g

commutes.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) (X : UU l3)
  where

  compute-coherence-triangle-fiber-precomp' :
    (g : A  X) 
    fiber (precomp f X) g  Σ (B  X)  h  coherence-triangle-maps' g h f)
  compute-coherence-triangle-fiber-precomp' g = equiv-tot  _  equiv-funext)

  compute-coherence-triangle-fiber-precomp :
    (g : A  X) 
    fiber (precomp f X) g  Σ (B  X)  h  coherence-triangle-maps g h f)
  compute-coherence-triangle-fiber-precomp g =
    equiv-tot  _  equiv-funext) ∘e equiv-fiber (precomp f X) g

  compute-fiber-precomp :
    (g : B  X) 
    fiber (precomp f X) (g  f) 
    Σ (B  X)  h  coherence-square-maps f f h g)
  compute-fiber-precomp g = compute-coherence-triangle-fiber-precomp (g  f)

  compute-total-fiber-precomp :
    Σ ( B  X)  g  fiber (precomp f X) (g  f)) 
    Σ (B  X)  u  Σ (B  X)  v  u  f ~ v  f))
  compute-total-fiber-precomp = equiv-tot compute-fiber-precomp

  diagonal-into-fibers-precomp :
    (B  X)  Σ (B  X)  g  fiber (precomp f X) (g  f))
  diagonal-into-fibers-precomp = map-section-family  g  g , refl)

The action on identifications of precomposition by a map

Consider a map f : A → B and two functions g h : B → C. Then the action on identifications of precomp f C fits in a commuting square

                     ap (precomp f C)
       (g = h) --------------------------> (g ∘ f = h ∘ f)
          |                                       |
  htpy-eq |                                       | htpy-eq
          ∨                                       ∨
       (g ~ h) --------------------------> (g ∘ f ~ h ∘ f).
                precomp f (eq-value g h)

Similarly, the action on identifications of precomp f C also fits in a commuting square

                precomp f (eq-value g h)
       (g ~ h) --------------------------> (g ∘ f ~ h ∘ f)
          |                                       |
  eq-htpy |                                       | eq-htpy
          ∨                                       ∨
       (g = h) --------------------------> (g ∘ f = h ∘ f).
                     ap (precomp f C)

commutes.

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

  compute-htpy-eq-ap-precomp :
    coherence-square-maps
      ( ap (precomp f C))
      ( htpy-eq)
      ( htpy-eq)
      ( precomp-Π f (eq-value g h))
  compute-htpy-eq-ap-precomp =
    compute-htpy-eq-ap-precomp-Π f

  compute-eq-htpy-ap-precomp :
    coherence-square-maps
      ( precomp-Π f (eq-value g h))
      ( eq-htpy)
      ( eq-htpy)
      ( ap (precomp f C))
  compute-eq-htpy-ap-precomp =
    vertical-inv-equiv-coherence-square-maps
      ( ap (precomp f C))
      ( equiv-funext)
      ( equiv-funext)
      ( precomp-Π f (eq-value g h))
      ( compute-htpy-eq-ap-precomp)

Recent changes