natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
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.
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:
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
Given types $A$, $B$, and $C$ and functions $f:A \to B$ and $g:A \to B$ there is a function
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)$
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
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$
Right whiskering is frequently written simply as $H \circ h$ or $H \cdot h$.
For whiskering in dependent type theory:
Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
For whiskering in category theory:
Peter Selinger: Introduction to categorical logic. pdf, page 41
Last revised on January 19, 2023 at 16:05:21. See the history of this page for a list of all contributions to it.