This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Whiskering identifications with respect to concatenation

module foundation.whiskering-identifications-concatenation where

open import foundation-core.whiskering-identifications-concatenation public
Imports 
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

Idea

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.

Properties

Left whiskering of identifications is an equivalence

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

  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 =
    is-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)
  where

  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 =
    is-equiv-right-whisker-concat