Precomposition of functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-04-25.

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
    ∨        ∨
    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