Postcomposition of functions

Content created by Fredrik Bakke and Egbert Rijke.

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

module foundation.postcomposition-functions where

open import foundation-core.postcomposition-functions public
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.postcomposition-dependent-functions
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.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-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.type-theoretic-principle-of-choice


Given a map f : X → Y and a type A, the postcomposition function

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

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


Postcomposition preserves homotopies

htpy-postcomp :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3) 
  {f g : X  Y}  (f ~ g)  postcomp A f ~ postcomp A g
htpy-postcomp A H h = eq-htpy (H ·r h)

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

Computations of the fibers of postcomp

We give three computations of the fibers of a postcomposition function:

  1. fiber (postcomp A f) h ≃ ((x : A) → fiber f (h x))
  2. fiber (postcomp A f) h ≃ Σ (A → X) (coherence-triangle-maps h f), and
  3. fiber (postcomp A f) (f ∘ h) ≃ Σ (A → X) (λ g → coherence-square-maps g h f f)
module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3)
  (f : X  Y)

  inv-compute-Π-fiber-postcomp :
    (h : A  Y)  fiber (postcomp A f) h  ((x : A)  fiber f (h x))
  inv-compute-Π-fiber-postcomp h =
    inv-distributive-Π-Σ ∘e equiv-tot  _  equiv-funext)

  compute-Π-fiber-postcomp :
    (h : A  Y)  ((x : A)  fiber f (h x))  fiber (postcomp A f) h
  compute-Π-fiber-postcomp h =
    equiv-tot  _  equiv-eq-htpy) ∘e distributive-Π-Σ

  inv-compute-coherence-triangle-fiber-postcomp :
    (h : A  Y) 
    fiber (postcomp A f) h  Σ (A  X) (coherence-triangle-maps h f)
  inv-compute-coherence-triangle-fiber-postcomp h =
    equiv-tot  _  equiv-funext) ∘e equiv-fiber (postcomp A f) h

  compute-coherence-triangle-fiber-postcomp :
    (h : A  Y) 
    Σ (A  X) (coherence-triangle-maps h f)  fiber (postcomp A f) h
  compute-coherence-triangle-fiber-postcomp h =
    inv-equiv (inv-compute-coherence-triangle-fiber-postcomp h)

  inv-compute-fiber-postcomp :
    (h : A  X) 
    fiber (postcomp A f) (f  h) 
    Σ (A  X)  g  coherence-square-maps g h f f)
  inv-compute-fiber-postcomp h =
    inv-compute-coherence-triangle-fiber-postcomp (f  h)

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

Postcomposition and equivalences

A map f is an equivalence if and only if postcomposing by f is an equivalence

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)
  (H : {l3 : Level} (A : UU l3)  is-equiv (postcomp A f))

  map-inv-is-equiv-is-equiv-postcomp : Y  X
  map-inv-is-equiv-is-equiv-postcomp = map-inv-is-equiv (H Y) id

  is-section-map-inv-is-equiv-is-equiv-postcomp :
    ( f  map-inv-is-equiv-is-equiv-postcomp) ~ id
  is-section-map-inv-is-equiv-is-equiv-postcomp =
    htpy-eq (is-section-map-inv-is-equiv (H Y) id)

  is-retraction-map-inv-is-equiv-is-equiv-postcomp :
    ( map-inv-is-equiv-is-equiv-postcomp  f) ~ id
  is-retraction-map-inv-is-equiv-is-equiv-postcomp =
      ( ap
        ( pr1)
        ( eq-is-contr
          ( is-contr-map-is-equiv (H X) f)
          { x =
              ( map-inv-is-equiv-is-equiv-postcomp  f) ,
              ( ap (_∘ f) (is-section-map-inv-is-equiv (H Y) id))}
          { y = id , refl}))

    is-equiv-is-equiv-postcomp : is-equiv f
    is-equiv-is-equiv-postcomp =

The following version of the same theorem works when X and Y are in the same universe. The condition of inducing equivalences by postcomposition is simplified to that universe.

is-equiv-is-equiv-postcomp' :
  {l : Level} {X : UU l} {Y : UU l} (f : X  Y) 
  ((A : UU l)  is-equiv (postcomp A f))  is-equiv f
is-equiv-is-equiv-postcomp' {l} {X} {Y} f is-equiv-postcomp-f =
  let section-f = center (is-contr-map-is-equiv (is-equiv-postcomp-f Y) id)
    ( pr1 section-f)
    ( htpy-eq (pr2 section-f))
    ( htpy-eq
      ( ap
        ( pr1)
        ( eq-is-contr'
          ( is-contr-map-is-equiv (is-equiv-postcomp-f X) f)
          ( pr1 section-f  f , ap (_∘ f) (pr2 section-f))
          ( id , refl))))

  is-equiv-postcomp-is-equiv :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)  is-equiv f 
    {l3 : Level} (A : UU l3)  is-equiv (postcomp A f)
  is-equiv-postcomp-is-equiv {X = X} {Y = Y} f is-equiv-f A =
      ( postcomp A (map-inv-is-equiv is-equiv-f))
      ( eq-htpy 
        right-whisker-comp (is-section-map-inv-is-equiv is-equiv-f))
      ( eq-htpy 
        right-whisker-comp (is-retraction-map-inv-is-equiv is-equiv-f))

  is-equiv-postcomp-equiv :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y) 
    {l3 : Level} (A : UU l3)  is-equiv (postcomp A (map-equiv f))
  is-equiv-postcomp-equiv f =
    is-equiv-postcomp-is-equiv (map-equiv f) (is-equiv-map-equiv f)

equiv-postcomp :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3) 
  (X  Y)  (A  X)  (A  Y)
pr1 (equiv-postcomp A e) = postcomp A (map-equiv e)
pr2 (equiv-postcomp A e) =
  is-equiv-postcomp-is-equiv (map-equiv e) (is-equiv-map-equiv e) A

Two maps being homotopic is equivalent to them being homotopic after pre- or postcomposition by an equivalence

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

  equiv-htpy-postcomp-htpy :
    (e : B  C) (f g : A  B)  (f ~ g)  (map-equiv e  f ~ map-equiv e  g)
  equiv-htpy-postcomp-htpy e f g =
    equiv-Π-equiv-family  a  equiv-ap e (f a) (g a))

Computing the action on identifications of postcomposition by a map

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

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

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

                          f ·l_
       (g ~ h) --------------------------> (g ∘ f ~ h ∘ f)
          |                                       |
  eq-htpy |                                       | eq-htpy
          ∨                                       ∨
       (g = h) --------------------------> (g ∘ f = h ∘ f).
                     ap (postcomp A f)
module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  {g h : A  B} (f : B  C)

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

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

Recent changes