Whiskering homotopies with respect to composition

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-02-06.
Last modified on 2024-04-17.

module foundation.whiskering-homotopies-composition where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

There are two whiskering operations on homotopies with respect to composition. The left whiskering operation of homotopies with respect to composition assumes a diagram of maps of the form

      f
    ----->     h
  A -----> B -----> C
      g

and is defined to be the function H ↦ h ·l H : (f ~ g) → (h ∘ f ~ h ∘ g). The right whiskering operation of homotopies with respect to composition assumes a diagram of maps the form

               g
      f      ----->
  A -----> B -----> C
               h

and is defined to be the function H ↦ H ·r f : (g ~ h) → (g ∘ f ~ h ∘ f).

Note. The infix whiskering operators _·l_ and _·r_ use the middle dot · (agda-input: \cdot \centerdot), as opposed to the infix homotopy concatenation operator _∙h_ which uses the bullet operator ∙ (agda-input: \.). If these look the same in your editor, we suggest that you change your font. For more details, see How to install.

Note. We will define the whiskering operations with respect to function composition for dependent functions. The definition of whiskering-operations in whiskering operations does not support this level of generality, so we will not be able to use it here.

Definitions

Left whiskering of homotopies

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

  left-whisker-comp :
    (h : {x : A} → B x → C x)
    {f g : (x : A) → B x} → f ~ g → h ∘ f ~ h ∘ g
  left-whisker-comp h H x = ap h (H x)

  infixr 17 _·l_
  _·l_ = left-whisker-comp

Right whiskering of homotopies

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  where

  right-whisker-comp :
    {g h : {x : A} (y : B x) → C x y}
    (H : {x : A} → g {x} ~ h {x})
    (f : (x : A) → B x) → g ∘ f ~ h ∘ f
  right-whisker-comp H f x = H (f x)

  infixl 16 _·r_
  _·r_ = right-whisker-comp

Double whiskering of homotopies

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2}
  {C : (x : A) → B x → UU l3} {D : (x : A) → B x → UU l4}
  where

  double-whisker-comp :
    (left : {x : A} {y : B x} → C x y → D x y)
    {g h : {x : A} (y : B x) → C x y}
    (H : {x : A} → g {x} ~ h {x})
    (right : (x : A) → B x) → left ∘ g ∘ right ~ left ∘ h ∘ right
  double-whisker-comp left H right = left ·l H ·r right

Properties

The left and right whiskering operations commute

We have the coherence

  (h ·l H) ·r h' ~ h ·l (H ·r h')

definitionally.

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2}
  {C : {x : A} → B x → UU l3} {D : {x : A} → B x → UU l4}
  {f g : {x : A} (y : B x) → C y}
  where

  coherence-double-whisker-comp :
    (h : {x : A} {y : B x} → C y → D y)
    (H : {x : A} → f {x} ~ g {x})
    (h' : (x : A) → B x) →
    (h ·l H) ·r h' ~ h ·l (H ·r h')
  coherence-double-whisker-comp h H h' = refl-htpy

Unit laws and absorption laws for whiskering homotopies

The identity map is a unit element for whiskerings from the function side, and the reflexivity homotopy is an absorbing element on the homotopy side for whiskerings.

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

  left-unit-law-left-whisker-comp :
    {f f' : (x : A) → B x} (H : f ~ f') → id ·l H ~ H
  left-unit-law-left-whisker-comp H x = ap-id (H x)

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

  right-absorption-law-left-whisker-comp :
    {f : (x : A) → B x} (g : {x : A} → B x → C x) →
    g ·l refl-htpy {f = f} ~ refl-htpy
  right-absorption-law-left-whisker-comp g = refl-htpy

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  where

  left-absorption-law-right-whisker-comp :
    {g : {x : A} (y : B x) → C x y} (f : (x : A) → B x) →
    refl-htpy {f = g} ·r f ~ refl-htpy
  left-absorption-law-right-whisker-comp f = refl-htpy

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

  right-unit-law-right-whisker-comp :
    {f f' : (x : A) → B x} (H : f ~ f') → H ·r id ~ H
  right-unit-law-right-whisker-comp H = refl-htpy

Laws for whiskering an inverted homotopy

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  {f f' : (x : A) → B x} (g : {x : A} → B x → C x) (H : f ~ f')
  where

  left-whisker-inv-htpy : g ·l (inv-htpy H) ~ inv-htpy (g ·l H)
  left-whisker-inv-htpy x = ap-inv g (H x)

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  {g g' : {x : A} (y : B x) → C x y} (H : {x : A} → g {x} ~ g' {x})
  (f : (x : A) → B x)
  where

  right-whisker-inv-htpy : inv-htpy H ·r f ~ inv-htpy (H ·r f)
  right-whisker-inv-htpy = refl-htpy

Inverse laws for whiskered homotopies

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  {f f' : (x : A) → B x} (g : {x : A} → B x → C x) (H : f ~ f')
  where

  left-inv-htpy-left-whisker : g ·l (inv-htpy H) ∙h g ·l H ~ refl-htpy
  left-inv-htpy-left-whisker =
    ( ap-concat-htpy' (g ·l H) (left-whisker-inv-htpy g H)) ∙h
    ( left-inv-htpy (g ·l H))

  right-inv-htpy-left-whisker : g ·l H ∙h g ·l (inv-htpy H) ~ refl-htpy
  right-inv-htpy-left-whisker =
    ( ap-concat-htpy (g ·l H) (left-whisker-inv-htpy g H)) ∙h
    ( right-inv-htpy (g ·l H))

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  {g g' : {x : A} (y : B x) → C x y} (H : {x : A} → g {x} ~ g' {x})
  (f : (x : A) → B x)
  where

  left-inv-htpy-right-whisker : (inv-htpy H) ·r f ∙h H ·r f ~ refl-htpy
  left-inv-htpy-right-whisker = left-inv-htpy (H ·r f)

  right-inv-htpy-right-whisker : H ·r f ∙h (inv-htpy H) ·r f ~ refl-htpy
  right-inv-htpy-right-whisker = right-inv-htpy (H ·r f)

Distributivity of whiskering over concatenation of homotopies

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

  distributive-left-whisker-comp-concat :
    { f g h : (x : A) → B x} (k : {x : A} → B x → C x) →
    ( H : f ~ g) (K : g ~ h) →
    k ·l (H ∙h K) ~ (k ·l H) ∙h (k ·l K)
  distributive-left-whisker-comp-concat k H K a =
    ap-concat k (H a) (K a)

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  (k : (x : A) → B x) {f g h : {x : A} (y : B x) → C x y}
  (H : {x : A} → f {x} ~ g {x}) (K : {x : A} → g {x} ~ h {x})
  where

  distributive-right-whisker-comp-concat :
    (H ∙h K) ·r k ~ (H ·r k) ∙h (K ·r k)
  distributive-right-whisker-comp-concat = refl-htpy

Whiskering preserves function composition

In other words, whiskering is an action of functions on homotopies.

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

  inv-preserves-comp-left-whisker-comp :
    ( k : {x : A} → C x → D x) (h : {x : A} → B x → C x) {f g : (x : A) → B x}
    ( H : f ~ g) →
    (k ∘ h) ·l H ~ k ·l (h ·l H)
  inv-preserves-comp-left-whisker-comp k h H x = ap-comp k h (H x)

  preserves-comp-left-whisker-comp :
    ( k : {x : A} → C x → D x) (h : {x : A} → B x → C x) {f g : (x : A) → B x}
    ( H : f ~ g) →
    k ·l (h ·l H) ~ (k ∘ h) ·l H
  preserves-comp-left-whisker-comp k h H =
    inv-htpy (inv-preserves-comp-left-whisker-comp k h H)

module _
  { l1 l2 l3 l4 : Level}
  { A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
  { D : (x : A) (y : B x) (z : C x y) → UU l4}
  { f g : {x : A} {y : B x} (z : C x y) → D x y z}
  ( h : {x : A} (y : B x) → C x y) (k : (x : A) → B x)
  ( H : {x : A} {y : B x} → f {x} {y} ~ g {x} {y})
  where

  preserves-comp-right-whisker-comp : (H ·r h) ·r k ~ H ·r (h ∘ k)
  preserves-comp-right-whisker-comp = refl-htpy

A coherence for homotopies to the identity function

Consider a function f : A → A and let H : f ~ id be a homotopy to the identity function. Then we have a homotopy

  H ·r f ~ f ·l H.

module _
  {l : Level} {A : UU l} {f : A → A} (H : f ~ id)
  where

  coh-htpy-id : H ·r f ~ f ·l H
  coh-htpy-id x = is-injective-concat' (H x) (nat-htpy-id H (H x))

  inv-coh-htpy-id : f ·l H ~ H ·r f
  inv-coh-htpy-id = inv-htpy coh-htpy-id

See also

Recent changes