Whiskering homotopies with respect to concatenation

Content created by Fredrik Bakke and Egbert Rijke.

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

module foundation.whiskering-homotopies-concatenation where

open import foundation-core.whiskering-homotopies-concatenation public
Imports 
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.homotopies

Idea

Consider a homotopy H : f ~ g and a homotopy K : I ~ J between two homotopies I J : g ~ f. The left whiskering of H and K is a homotopy H ∙h I ~ H ∙h J. In other words, left whiskering of homotopies with respect to concatenation is a whiskering operation

  (H : f ~ g) {I J : g ~ h} → I ~ J → H ∙h I ~ H ∙h K.

Similarly, we introduce right whiskering to be an operation

  {H I : f ~ g} → H ~ I → (J : g ~ h) → H ∙h J ~ I ∙h J.

Properties

Left whiskering of homotopies with respect to concatenation is an equivalence

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

  is-equiv-left-whisker-concat-htpy :
    {f g h : (x : A) → B x} (H : f ~ g) {I J : g ~ h} →
    is-equiv (left-whisker-concat-htpy H {I} {J})
  is-equiv-left-whisker-concat-htpy H =
    is-equiv-map-Π-is-fiberwise-equiv
      ( λ x → is-equiv-left-whisker-concat (H x))

Right whiskering of homotopies with respect to concatenation is an equivalence

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

  is-equiv-right-whisker-concat-htpy :
    {f g h : (x : A) → B x} {H I : f ~ g} (J : g ~ h) →
    is-equiv (λ (K : H ~ I) → right-whisker-concat-htpy K J)
  is-equiv-right-whisker-concat-htpy J =
    is-equiv-map-Π-is-fiberwise-equiv
      ( λ x → is-equiv-right-whisker-concat (J x))

Recent changes