Loading [MathJax]/extensions/TeX/HTML.js

Sunday, April 6, 2014

Quantification as 2-categorical extension

First, as to the title:
We are considering quantification as extension within a 2-category,
not the problem of extending 2-functors between 2-categories.

For now, I am going to skip the preliminaries and introduction
and just give a diagram in
the 2-category Cat of small categories, functors, and natural transformations
showing how quantification is an extension in that 2-category.
Here \leftcat X and \rightcat Y are the discrete categories associated to (small) sets with the same names (sorry for the overloading of the notation!).
We have a function \leftcat X \xrightarrow f \rightcat Y
which we may consider as a functor between the discrete categories.
2 is the category associated to the total order 2 = \{\,0\lt 1\,\} = \{\,\bot \lt \top\,\}.
\begin{array}{} && \rightcat 1 & \target{\mathop\rightarrowtail\limits^y} & \rightcat Y & \rightcat = & \rightcat Y\\ & \nearrow & \Uparrow & \llap{\raise3pt\hbox{$f\!\!\!$}}\nearrow & \leftadj\Uparrow & \leftadj\searrow\rlap{\raise3pt\hbox{$\!\!\leftadj\exists_f \leftcat A$}} & \quad\rightcat\Rightarrow & \rightcat{\searrow\rlap{\raise3pt\hbox{$\!\!\!B$}}}\\ f\rightcat{{\downarrow}y} & \rightarrowtail & \leftcat X & & \leftcat{\xrightarrow[\textstyle A]{}} & & 2 & = & 2\\ \big\uparrow && \big\uparrow && \big\Uparrow && \big\uparrow\rlap\top\\ f\rightcat{{\downarrow}y} \cap \top\leftcat{{\downarrow}A} & \rightarrowtail & \top\leftcat{{\downarrow}A} && \rightarrow && 1\\ \end{array} In that situation \leftadj\exists_f \source A is a left extension of \leftcat A over f, as shown.
I.e., for all (predicates B on Y),
(2-cells from the predicate A on X to f\rightcat B)
correspond uniquely and naturally to
(2-cells from \leftadj\exists_f \source A to B).

No comments:

Post a Comment

MathJax 2.7.9