Whiskering identifications with respect to concatenation

Content created by Fredrik Bakke and Egbert Rijke.

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

module foundation.whiskering-identifications-concatenation where

open import foundation-core.whiskering-identifications-concatenation public
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-operations

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


Consider two identifications p q : x = y in a type A. The whiskering operations are operations that take identifications p = q to identifications r ∙ p = r ∙ q or to identifications p ∙ r = q ∙ r.

The left whiskering operation takes an identification r : z = x and an identification p = q to an identification r ∙ p = r ∙ q. Similarly, the right whiskering operation takes an identification r : y = z and an identification p = q to an identification p ∙ r = q ∙ r.

The whiskering operations can be defined by the acion on identifications of concatenation. Since concatenation on either side is an equivalence, it follows that the whiskering operations are equivalences.


Left whiskering of identifications is an equivalence

module _
  {l : Level} {A : UU l} {x y z : A} (p : x  y) {q q' : y  z}

  is-equiv-left-whisker-concat :
    is-equiv (left-whisker-concat p {q} {q'})
  is-equiv-left-whisker-concat =
    is-emb-is-equiv (is-equiv-concat p z) q q'

  equiv-left-whisker-concat : (q  q')  (p  q  p  q')
  pr1 equiv-left-whisker-concat =
    left-whisker-concat p
  pr2 equiv-left-whisker-concat =

Right whiskering of identification is an equivalence

module _
  {l : Level} {A : UU l} {x y z : A} {p p' : x  y} (q : y  z)

  is-equiv-right-whisker-concat :
    is-equiv  (α : p  p')  right-whisker-concat α q)
  is-equiv-right-whisker-concat =
    is-emb-is-equiv (is-equiv-concat' x q) p p'

  equiv-right-whisker-concat : (p  p')  (p  q  p'  q)
  pr1 equiv-right-whisker-concat α =
    right-whisker-concat α q
  pr2 equiv-right-whisker-concat =

Recent changes