Whiskering homotopies with respect to concatenation

Content created by Fredrik Bakke.

Created on 2024-02-19.
Last modified on 2024-02-19.

module foundation-core.whiskering-homotopies-concatenation where
Imports 
open import foundation.universe-levels
open import foundation.whiskering-operations

open import foundation-core.homotopies
open import foundation-core.whiskering-identifications-concatenation

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.

Definitions

Left whiskering of homotopies with respect to concatenation

Left whiskering of homotopies with respect to concatenation is an operation

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

We implement the left whiskering operation of homotopies with respect to concatenation as an instance of a general left whiskering operation.

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

  left-whisker-concat-htpy :
    left-whiskering-operation ((x : A) → B x) (_~_) (_∙h_) (_~_)
  left-whisker-concat-htpy H K x = left-whisker-concat (H x) (K x)

  left-unwhisker-concat-htpy :
    {f g h : (x : A) → B x} (H : f ~ g) {I J : g ~ h} → H ∙h I ~ H ∙h J → I ~ J
  left-unwhisker-concat-htpy H K x = left-unwhisker-concat (H x) (K x)

Right whiskering of homotopies with respect to concatenation

Right whiskering of homotopies with respect to concatenation is an operation

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

We implement the right whiskering operation of homotopies with respect to concatenation as an instance of a general right whiskering operation.

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

  right-whisker-concat-htpy :
    right-whiskering-operation ((x : A) → B x) (_~_) (_∙h_) (_~_)
  right-whisker-concat-htpy K J x = right-whisker-concat (K x) (J x)

  right-unwhisker-concat-htpy :
    {f g h : (x : A) → B x} {H I : f ~ g} (J : g ~ h) → H ∙h J ~ I ∙h J → H ~ I
  right-unwhisker-concat-htpy H K x = right-unwhisker-concat (H x) (K x)

Properties

The unit and absorption laws for left whiskering of homotopies with respect to concatenation

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

  left-unit-law-left-whisker-concat-htpy :
    {f g : (x : A) → B x} {I J : f ~ g} (K : I ~ J) →
    left-whisker-concat-htpy refl-htpy K ~ K
  left-unit-law-left-whisker-concat-htpy K x =
    left-unit-law-left-whisker-concat (K x)

  right-absorption-law-left-whisker-concat-htpy :
    {f g h : (x : A) → B x} (H : f ~ g) {I : g ~ h} →
    left-whisker-concat-htpy H (refl-htpy' I) ~ refl-htpy
  right-absorption-law-left-whisker-concat-htpy H x =
    right-absorption-law-left-whisker-concat (H x) _

The unit and absorption laws for right whiskering of homotopies with respect to concatenation

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

  left-absorption-law-right-whisker-concat-htpy :
    {f g h : (x : A) → B x} {H : f ~ g} (J : g ~ h) →
    right-whisker-concat-htpy (refl-htpy' H) J ~ refl-htpy
  left-absorption-law-right-whisker-concat-htpy J x =
    left-absorption-law-right-whisker-concat _ (J x)

  right-unit-law-right-whisker-concat-htpy :
    {f g : (x : A) → B x} {I J : f ~ g} (K : I ~ J) →
    right-unit-htpy ∙h K ~
    right-whisker-concat-htpy K refl-htpy ∙h right-unit-htpy
  right-unit-law-right-whisker-concat-htpy K x =
    right-unit-law-right-whisker-concat (K x)

Recent changes