# nLab whiskering

Whiskering

### Context

#### 2-Category theory

2-category theory

Definitions

Transfors between 2-categories

Morphisms in 2-categories

Structures in 2-categories

Limits in 2-categories

Structures on 2-categories

# Whiskering

## Idea

In a 2-category, the horizontal composition of a 2-morphism with 1-morphisms is sometimes called whiskering.

Whiskering from the left with an equivalence and from the right with an inverse equivalence is a conjugation action of equivalences on 2-morphisms.

## Examples

An important use of whiskering is the usual definition of adjoint functors via the triangle identities: in Cat whiskering is the composition of a functor with a natural transformation to produce a natural transformation.

If we identify a functor or 1-morphism with its identity natural transformation or identity 2-morphism?, then whiskering is a special case of horizontal composition, and composition of 1-morphisms is a special case of whiskering.

In detail:

• If $F,G\colon C \to D$ and $H\colon D\to E$ are functors and $\eta\colon F \to G$ is a natural transformation whose coordinate at any object $A$ of $C$ is $\eta_A$, then whiskering $H$ and $\eta$ yields the natural transformation $H \circ \eta\colon (H \circ F) \to (H \circ G)$ whose coordinate at $A$ is $H(\eta_A)$.
• If $F\colon C \to D$ and $G,H\colon D \to E$ are functors and $\eta\colon G\to H$ is a natural transformation whose coordinate at $A$ is $\eta_A$, then whiskering $\eta$ and $F$ yields the natural transformation $\eta \circ F\colon (G \circ F) \to (H \circ F)$ whose coordinate at $A$ is $\eta_{F(A)}$.

## In dependent type theory

In dependent type theory, whiskering is the type theoretic equivalent of the principle in set theory that given sets $A$, $B$, and $C$, and functions $f:A \to B$ and $g:A \to B$, if $f(x) = g(x)$ for all elements $x \in A$, then

• $h(f(x)) = h(g(x))$ for all functions $h:B \to C$ and elements $x \in A$
• $f(h(x)) = g(h(x))$ for all functions $h:C \to A$ and elements $x \in C$

Given types $A$, $B$, and $C$ and functions $f:A \to B$ and $g:A \to B$ there is a function

$\mathrm{leftwhiskering}_{A, B, C}(f, g):\left(\prod_{x:A} f(x) =_B g(x)\right) \to \left(\prod_{h:B \to C} \prod_{x:A} h(f(x)) =_C h(g(x))\right)$

called left whiskering, which is defined as the lambda abstraction of the composite of the function application to identities of function $h:B \to C$ with homotopy $H:\prod_{x:A} f(x) =_B g(x)$

$\mathrm{leftwhiskering}_{A, B, C}(f, g)(H, h) \coloneqq \lambda x.\mathrm{ap}_h(H(x))$

Left whiskering is frequently written simply as $h \circ H$ or $h \cdot H$.

Given types $A$, $B$, and $C$ and functions $f:A \to B$ and $g:A \to B$, there is a function

$\mathrm{rightwhiskering}_{A, B, C}(f, g):\left(\prod_{x:A} f(x) =_B g(x)\right) \to \left(\prod_{h:C \to A} \prod_{x:C} f(h(x)) =_B g(h(x))\right)$

called right whiskering, defined as the lambda abstraction of the composite of homotopy $H:\prod_{x:A} f(x) =_B g(x)$ with function $h:C \to A$

$\mathrm{rightwhiskering}_{A, B, C}(f, g)(H, h) \coloneqq \lambda x.H(h(x))$

Right whiskering is frequently written simply as $H \circ h$ or $H \cdot h$.

For whiskering in dependent type theory:

For whiskering in category theory: