# Whiskering identifications with respect to concatenation

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-02-06.

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