Whiskering higher homotopies with respect to composition

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2024-02-06.
Last modified on 2024-03-13.

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

open import foundation-core.homotopies

Idea

Consider two dependent functions f g : (x : A) → B x equipped with two homotopies H H' : f ~ g, and consider a family of maps h : (x : A) → B x → C x. Then we obtain a map

  α ↦ ap h ·l α : H ~ H' → h ·l H ~ h ·l H'

This operation is called the left whiskering. Alternatively the left whiskering operation of 2-homotopies can be defined using the action on higher identifications of functions by

  α x ↦ ap² h (α x).

Similarly, the right whiskering is defined to be the operation

  (H ~ H') → (h : (x : A) → B x) → (H ·r h ~ H' ·r h)

given by

  α h ↦ α ·r h,

for any pair of homotopies H H' : f ~ g, where f g : (x : A) (y : B x) → C x y.

Definitions

Left whiskering higher homotopies

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

  left-whisker-comp² :
    (h : {x : A} → B x → C x) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H'
  left-whisker-comp² h α = ap h ·l α

Right whiskering higher homotopies

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

  right-whisker-comp² :
    (α : {x : A} → H {x} ~ H' {x}) (h : (x : A) → B x) → H ·r h ~ H' ·r h
  right-whisker-comp² α h = α ·r h

Double whiskering higher 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}
  {f g : {x : A} (y : B x) → C x y} {H H' : {x : A} → f {x} ~ g {x}}
  where

  double-whisker-comp² :
    (left : {x : A} {y : B x} → C x y → D x y)
    (α : {x : A} → H {x} ~ H' {x})
    (right : (x : A) → B x) →
    left ·l H ·r right ~ left ·l H' ·r right
  double-whisker-comp² left α right = double-whisker-comp (ap left) α right

Recent changes