Whiskering homotopies

Content created by Egbert Rijke

Created on 2023-09-12.
Last modified on 2023-09-12.

module foundation.whiskering-homotopies where

open import foundation-core.whiskering-homotopies public
Imports 
open import foundation.action-on-identifications-functions
open import foundation.function-extensionality
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. The left whiskering operation assumes a diagram of the form

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

and is defined to be a function h ·l_ : (f ~ g) → (h ∘ f ~ h ∘ g). The right whiskering operation assumes a diagram of the form

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

and is defined to be a function _·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.

Properties

Computation of function extensionality on whiskerings

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

  compute-eq-htpy-htpy-eq-right-whisk :
    ( p : f ＝ g) →
    eq-htpy ((htpy-eq p) ·r h) ＝ ap (precomp h C) p
  compute-eq-htpy-htpy-eq-right-whisk refl =
    eq-htpy-refl-htpy (f ∘ h)

  compute-eq-htpy-right-whisk :
    ( H : f ~ g) →
    eq-htpy (H ·r h) ＝ ap (precomp h C) (eq-htpy H)
  compute-eq-htpy-right-whisk H =
    ( ap
      ( λ K → eq-htpy (K ·r h))
      ( inv (is-section-eq-htpy H))) ∙
    ( compute-eq-htpy-htpy-eq-right-whisk (eq-htpy H))

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

  compute-eq-htpy-htpy-eq-left-whisk :
    ( p : f ＝ g) →
    eq-htpy ( h ·l (htpy-eq p)) ＝ ap (postcomp A h) p
  compute-eq-htpy-htpy-eq-left-whisk refl =
    eq-htpy-refl-htpy (h ∘ f)

  compute-eq-htpy-left-whisk :
    (H : f ~ g) →
    eq-htpy (h ·l H) ＝ ap (postcomp A h) (eq-htpy H)
  compute-eq-htpy-left-whisk H =
    ( ap
      ( λ K → eq-htpy (h ·l K))
      ( inv (is-section-eq-htpy H))) ∙
    ( compute-eq-htpy-htpy-eq-left-whisk (eq-htpy H))

Recent changes