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$).