Whiskering identifications with respect to concatenation

Content created by Fredrik Bakke.

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

module foundation-core.whiskering-identifications-concatenation where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.universe-levels
open import foundation.whiskering-operations

open import foundation-core.homotopies
open import foundation-core.identity-types

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.

Definitions

Left whiskering of identifications

Left whiskering of identifications with respect to concatenation is an operation

  (p : x ＝ y) {q r : y ＝ z} → q ＝ r → p ∙ q ＝ p ∙ r

on any type.

module _
  {l : Level} {A : UU l}
  where

  left-whisker-concat : left-whiskering-operation A (_＝_) (_∙_) (_＝_)
  left-whisker-concat p β = ap (p ∙_) β

  left-unwhisker-concat :
    {x y z : A} (p : x ＝ y) {q r : y ＝ z} → p ∙ q ＝ p ∙ r → q ＝ r
  left-unwhisker-concat = is-injective-concat

Right whiskering of identifications

Right whiskering of identifications with respect to concatenation is an operation

  {p q : x ＝ y} → p ＝ q → (r : y ＝ z) → p ∙ r ＝ q ∙ r

on any type.

module _
  {l : Level} {A : UU l}
  where

  right-whisker-concat : right-whiskering-operation A (_＝_) (_∙_) (_＝_)
  right-whisker-concat α q = ap (_∙ q) α

  right-unwhisker-concat :
    {x y z : A} {p q : x ＝ y} (r : y ＝ z) → p ∙ r ＝ q ∙ r → p ＝ q
  right-unwhisker-concat r = is-injective-concat' r

Double whiskering of identifications

module _
  {l : Level} {A : UU l}
  {a b c d : A} (p : a ＝ b) {r s : b ＝ c} (t : r ＝ s) (q : c ＝ d)
  where

  double-whisker-concat : (p ∙ r) ∙ q ＝ (p ∙ s) ∙ q
  double-whisker-concat = right-whisker-concat (left-whisker-concat p t) q

  double-whisker-concat' : p ∙ (r ∙ q) ＝ p ∙ (s ∙ q)
  double-whisker-concat' = left-whisker-concat p (right-whisker-concat t q)

Properties

The unit and absorption laws for left whiskering of identifications

module _
  {l : Level} {A : UU l}
  where

  left-unit-law-left-whisker-concat :
    {x y : A} {p p' : x ＝ y} (α : p ＝ p') →
    left-whisker-concat refl α ＝ α
  left-unit-law-left-whisker-concat refl = refl

  right-absorption-law-left-whisker-concat :
    {x y z : A} (p : x ＝ y) (q : y ＝ z) →
    left-whisker-concat p (refl {x = q}) ＝ refl
  right-absorption-law-left-whisker-concat p q = refl

The unit and absorption laws for right whiskering of identifications

The right unit law for right whiskering of identifications with respect to concatenation asserts that the square of identifications

                     right-whisker-concat α refl
           p ∙ refl -----------------------------> p' ∙ refl
             |                                        |
  right-unit |                                        |
             ∨                                        ∨
             p -------------------------------------> p'

commutes for any α : p ＝ p'. Note that this law is slightly more complicated, since concatenating with refl on the right does not compute to the identity function.

module _
  {l : Level} {A : UU l}
  where

  right-unit-law-right-whisker-concat :
    {x y : A} {p p' : x ＝ y} (α : p ＝ p') →
    right-unit ∙ α ＝ right-whisker-concat α refl ∙ right-unit
  right-unit-law-right-whisker-concat {p = refl} refl = refl

  left-absorption-law-right-whisker-concat :
    {x y z : A} (p : x ＝ y) (q : y ＝ z) →
    right-whisker-concat (refl {x = p}) q ＝ refl
  left-absorption-law-right-whisker-concat p q = refl

Commutativity of left and right whiskering of identifications

Consider four identifications p p' : x ＝ y and q q' : y ＝ z in a type A. Then the square of identifications

                         right-whisker α q
                 p ∙ q ---------------------> p' ∙ q
                   |                             |
  left-whisker p β |                             | left-whisker p' β
                   ∨                             ∨
                 p ∙ q' --------------------> p' ∙ q'
                         right-whisker α q'

commutes. There are at least two natural ways in which this square is seen to commute:

  1. The square commutes by naturality of the homotopy α ↦ left-whisker-concat α β.
  2. The transposed square commutes by the naturality of the homotopy β ↦ right-whisker-concat α β.

These two ways in which the square commutes are inverse to each other.

Note. The following statements could have been formalized using commuting squares of identifications. However, in order to avoid cyclic module dependencies in the library we avoid doing so.

module _
  {l : Level} {A : UU l} {x y z : A}
  where

  commutative-left-whisker-right-whisker-concat :
    {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
    left-whisker-concat p β ∙ right-whisker-concat α q' ＝
    right-whisker-concat α q ∙ left-whisker-concat p' β
  commutative-left-whisker-right-whisker-concat β =
    nat-htpy (λ α → left-whisker-concat α β)

  commutative-right-whisker-left-whisker-concat :
    {p p' : x ＝ y} (α : p ＝ p') {q q' : y ＝ z} (β : q ＝ q') →
    right-whisker-concat α q ∙ left-whisker-concat p' β ＝
    left-whisker-concat p β ∙ right-whisker-concat α q'
  commutative-right-whisker-left-whisker-concat α =
    nat-htpy (right-whisker-concat α)

  compute-inv-commutative-left-whisker-right-whisker-concat :
    {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
    inv (commutative-right-whisker-left-whisker-concat α β) ＝
    commutative-left-whisker-right-whisker-concat β α
  compute-inv-commutative-left-whisker-right-whisker-concat refl refl =
    refl

Swapping the order of left and right whiskering of identifications

Consider a diagram of identifications

               r
      p      ----->     q
  a -----> b -----> c ----->
               s

with t : r ＝ s. Then the square of identifications

                               assoc p r q
                  (p ∙ r) ∙ q -------------> p ∙ (r ∙ q)
                       |                          |
  double-whisker p t q |                          | double-whisker' p t q
                       ∨                          ∨
                  (p ∙ s) ∙ q -------------> p ∙ (s ∙ q)
                               assoc p s q

commutes.

module _
  {l1 : Level} {A : UU l1}
  where

  swap-double-whisker-concat :
    {a b c d : A} (p : a ＝ b) {r s : b ＝ c} (t : r ＝ s) (q : c ＝ d) →
    double-whisker-concat p t q ∙ assoc p s q ＝
    assoc p r q ∙ double-whisker-concat' p t q
  swap-double-whisker-concat refl refl refl = refl

The action on identifications of concatenating by refl on the right

Consider an identification r : p ＝ q between two identifications p q : x ＝ y in a type A. Then the square of identifications

                      right-whisker r refl
            p ∙ refl ----------------------> q ∙ refl
              |                                |
   right-unit |                                | right-unit
              ∨                                ∨
              p -----------------------------> q
                                r

commutes.

module _
  {l : Level} {A : UU l} {x y : A} {p q : x ＝ y}
  where

  compute-refl-right-whisker-concat :
    (r : p ＝ q) →
    right-unit ∙ r ＝ right-whisker-concat r refl ∙ right-unit
  compute-refl-right-whisker-concat refl = right-unit

Left whiskering of identifications distributes over concatenation

module _
  {l : Level} {A : UU l}
  where

  distributive-left-whisker-concat-concat :
    {a b c : A} (p : a ＝ b) {q r s : b ＝ c} (α : q ＝ r) (β : r ＝ s) →
    left-whisker-concat p (α ∙ β) ＝
    left-whisker-concat p α ∙ left-whisker-concat p β
  distributive-left-whisker-concat-concat p refl β = refl

Right whiskering of identifications distributes over concatenation

module _
  {l : Level} {A : UU l}
  where

  distributive-right-whisker-concat-concat :
    {a b c : A} {p q r : a ＝ b} (α : p ＝ q) (β : q ＝ r) (s : b ＝ c) →
    right-whisker-concat (α ∙ β) s ＝
    right-whisker-concat α s ∙ right-whisker-concat β s
  distributive-right-whisker-concat-concat refl β s = refl

Left whiskering of identifications commutes with inverses of identifications

module _
  {l : Level} {A : UU l}
  where

  compute-inv-left-whisker-concat :
    {a b c : A} (p : a ＝ b) {q r : b ＝ c} (s : q ＝ r) →
    left-whisker-concat p (inv s) ＝ inv (left-whisker-concat p s)
  compute-inv-left-whisker-concat p s = ap-inv (concat p _) s

Right whiskering of identifications commutes with inverses of identifications

module _
  {l : Level} {A : UU l}
  where

  compute-inv-right-whisker-concat :
    {a b c : A} {p q : a ＝ b} (s : p ＝ q) (r : b ＝ c) →
    right-whisker-concat (inv s) r ＝ inv (right-whisker-concat s r)
  compute-inv-right-whisker-concat s r = ap-inv (concat' _ r) s

Recent changes