\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{2-category equipped with proarrows} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{2category_theory}{}\paragraph*{{2-Category theory}}\label{2category_theory} [[!include 2-category theory - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{motivation}{Motivation}\dotfill \pageref*{motivation} \linebreak \noindent\hyperlink{Definitions}{Definitions}\dotfill \pageref*{Definitions} \linebreak \noindent\hyperlink{DefinitionAsA2Functor}{Definition as a 2-functor}\dotfill \pageref*{DefinitionAsA2Functor} \linebreak \noindent\hyperlink{terminology}{Terminology}\dotfill \pageref*{terminology} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{DefinitionAsDoubleCategory}{Definition as a double category}\dotfill \pageref*{DefinitionAsDoubleCategory} \linebreak \noindent\hyperlink{as_a_category_internal_to_}{As a category internal to $Cat$}\dotfill \pageref*{as_a_category_internal_to_} \linebreak \noindent\hyperlink{related_notions}{Related notions}\dotfill \pageref*{related_notions} \linebreak \noindent\hyperlink{category_theory_in_a_proarrow_equipment}{Category theory in a proarrow equipment}\dotfill \pageref*{category_theory_in_a_proarrow_equipment} \linebreak \noindent\hyperlink{HomsetAdjn}{Homset definition of adjunctions}\dotfill \pageref*{HomsetAdjn} \linebreak \noindent\hyperlink{fully_faithful_arrows}{Fully faithful arrows}\dotfill \pageref*{fully_faithful_arrows} \linebreak \noindent\hyperlink{limits}{Limits}\dotfill \pageref*{limits} \linebreak \noindent\hyperlink{right_adjoints_preserve_limits}{Right adjoints preserve limits}\dotfill \pageref*{right_adjoints_preserve_limits} \linebreak \noindent\hyperlink{graphs_and_cographs}{Graphs and cographs}\dotfill \pageref*{graphs_and_cographs} \linebreak \noindent\hyperlink{virtual_equipments}{Virtual equipments}\dotfill \pageref*{virtual_equipments} \linebreak \noindent\hyperlink{CategoriesEnrichedInAnEquipment}{Categories enriched in an equipment}\dotfill \pageref*{CategoriesEnrichedInAnEquipment} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \textbf{2-category equipped with proarrows}, also called a \emph{proarrow equipment} or simply an \emph{equipment}, is a [[2-category]] together with extra ``proarrows'' which enable one to reproduce more category theory inside it than is possible in a general 2-category. The ur-example is [[Cat]] equipped with [[profunctors]]. See also [[framed bicategory]]. \hypertarget{motivation}{}\subsection*{{Motivation}}\label{motivation} Just as ordinary [[category theory]] provides a framework in which one can do ``formal mathematics,'' one of the (many) purposes of [[higher category theory]] is to provide a framework in which one can do ``formal category theory.'' In particular, many concepts in ordinary category theory can be interpreted internally in a [[2-category]], in a way which specializes to the original concept in [[Cat]]. Examples of such concepts include [[adjunctions]], [[monads]], [[Grothendieck fibrations]], [[Kan extensions]], and [[fully faithful morphisms]]. However, these internalizations are not always ``correct'' in every 2-category. For instance, in the 2-category $V Cat$ of [[enriched categories|categories enriched]] in a [[monoidal category]] $V$, internal adjunctions and monads give the correct notion of $V$-adjunction and $V$-monad, but internal fully-faithfulness for a $V$-functor is weaker than the ``correct'' notion of $V$-fully-faithfulness. More technically, in many cases the naive notion of Kan extension is not sufficient and one needs ``pointwise'' Kan extensions; with some more work these can also be defined in a 2-category, but the resulting notion (though correct in $Cat$) is not always correct in $V Cat$. Furthermore, some concepts of category theory are difficult to interpret at all in a 2-category. The notion of [[limit]] in ordinary category theory can be interpreted in a 2-category by identifying the limit of a functor $D\to C$ as its Kan extension along the unique functor $D\to *$. However, in enriched category theory the more important notion is that of [[weighted limit]], and there is no straightforward way to interpret this in $V Cat$. What is missing is that the 2-category $V Cat$ doesn't natively supply any information about the $V$-valued hom-functors in a 2-category. (In $Cat$ these hom-functors can be recovered by looking at [[comma categories]], which can be interpreted internally as [[comma objects]]---in some sense this is what all the above internalizations are secretly doing.) Thus, all of these problems can be remedied by equipping a 2-category with extra structure which describes these hom-functors, or more generally describes a notion of [[profunctor]]. There are several not-quite-equivalent ways to describe this extra structure. One due to Street and Walters, called a [[Yoneda structure]], involves assigning to each object $A$ a ``presheaf object'' $P A$ and a ``Yoneda arrow'' $A\to P A$; a profunctor $A\to B$ is then identified with an arrow $B \to P A$. The notion of \emph{proarrow equipment}, due to Wood, instead postulates an additional bicategory of ``proarrows'' and specifies their relationship to the ordinary arrows. One can then define fully faithful morphisms, pointwise Kan extensions, weighted limits, etc. relative to this structure, in a way which specializes to the correct notions in $V Cat$. \hypertarget{Definitions}{}\subsection*{{Definitions}}\label{Definitions} There are several equivalent ways to define proarrow equipments on a 2-category. \hypertarget{DefinitionAsA2Functor}{}\subsubsection*{{Definition as a 2-functor}}\label{DefinitionAsA2Functor} Let $K$ be a [[2-category]]. The following structure is said to \textbf{equip $K$ with proarrows}. \begin{itemize}% \item A 2-category $M$, whose arrows are called \emph{proarrows}. \item A functor $K\to M$ which is [[bijective-on-objects functor|bijective on objects]] and [[locally fully faithful 2-functor|locally fully faithful]]. If $f\colon A\to B$ is a 1-morphism in $K$, we write its image in $M$ as $B(1,f)\colon A\nrightarrow B$. \item For each arrow $f\colon A\to B$ in $K$, the proarrow $B(1,f)\colon A\to B$ has a [[right adjoint]] in $M$, which we write as $B(f,1)$. \end{itemize} As usual on the nLab, here by [[2-category]] we mean a weak 2-category (aka [[bicategory]]) and by [[functor]] we mean a weak 2-functor (aka [[pseudofunctor]]). However, in many or most examples, $K$ is in fact a [[strict 2-category]]. For a proarrow $H\colon B\to D$ and ordinary arrows $f\colon A\to B$ and $g\colon C\to D$, we write $H(g,f)$ for the composite $D(g,1) \circ H \circ B(1,f)$; it is a proarrow from $A$ to $C$. We also write $U_A$, $A(1,1)$, or simply $A$ for the identity proarrow $A\nrightarrow A$. Note that in the case where proarrows are profunctors, $H(g, f)$ is not the action on a set of [[heteromorphisms]] by pre- and post- composing with morphisms; instead it is the functor $f$, followed by the profunctor $H$, followed by taking the preimage under the functor $g$, resulting in a profunctor from $A$ to $C$. \hypertarget{terminology}{}\paragraph*{{Terminology}}\label{terminology} We refer to the entire structure defined above as a \textbf{2-category equipped with proarrows} or a \textbf{2-category proarrow equipment}. Those working in the field often use the term \textbf{proarrow equipment} or simply \textbf{equipment} for the entire structure. We prefer ``2-category equipped with proarrows'' (or, equivalently, ``pro-morphisms'') for the following reasons: \begin{itemize}% \item It conveys that we are talking about extra stuff added to a 2-category. (Actually, it is ``eka-stuff'' or ``2-stuff'' in the sense of \href{http://ncatlab.org/nlab/show/stuff,+structure,+property}{stuff, structure, property}.) \item It includes the word ``proarrow'' which tells people what the extra stuff consists of, namely a generalization of [[profunctors]]. \item It includes the word ``equipment'' which signals what is meant to readers who are familiar with that term. \end{itemize} We do sometimes avail ourselves of the shorter terminology ``proarrow equipment,'' however, once we are clear what is under discussion. \hypertarget{examples}{}\paragraph*{{Examples}}\label{examples} For example, if $V$ is a (Benabou) [[cosmos]], the 2-category $K= V Cat$ of $V$-enriched categories is equipped with proarrows by the 2-category $M=V Mod$ of $V$-enriched profunctors, where $B(1,f)$ and $B(f,1)$ are the two ways of regarding a $V$-functor $f:A\to B$ as a profunctor, namely $B(-,f-)$ and $B(f-,-)$ (hence the notation in the general case). Composition of $V$-profunctors is by [[tensor product]], i.e. [[coends]]; note that we require $V$ to be [[cocomplete category|cocomplete]] with colimits preserved by $\otimes$ on both sides in order to form such associative tensor products. In $V Cat$, $H(g,f)$ is the result of precomposing the profunctor $H:D^{op}\otimes B \to V$ with $g^{op}\otimes f$. The other most common sorts of generalized category, such as [[internal categories]] in some category with pullbacks, and [[fibered categories]] over some base, are also naturally equipped with proarrows. For internal categories in $S$, we require $S$ to have finite limits and coequalizers preserved by pullback in order for the bicategory of internal profunctors to have associative compositions. (See ``virtual equipments,'' below, for a context which avoids some of these restrictions on $V$ and $S$.) \hypertarget{DefinitionAsDoubleCategory}{}\subsubsection*{{Definition as a double category}}\label{DefinitionAsDoubleCategory} We discuss now how a 2-category with proarrow equipment is equivalently a [[double category]] with extra structure. Given a 2-category $K$ equipped with proarrows, we can construct a [[double category]] having the same objects as $K$, whose vertical 1-cells are the arrows, whose horizontal 1-cells are the proarrows, and whose squares \begin{displaymath} \itexarray{A & \overset{H}{\to} & C \\ ^f\downarrow & \Downarrow & \downarrow^g\\ B& \underset{J}{\to} & D} \end{displaymath} are the 2-cells $H \to J(g,f)$. Note that if $K$ is a strict 2-category, then this is a [[pseudo double category]] (vertically strict and horizontally weak) while if $K$ and $M$ are both weak 2-categories, this double category is weak in both directions (like a [[double bicategory]]). In $V Cat$, for example, the squares of the above form are transformations $H(b,a) \to J(g b,f a)$ natural in $a$ and $b$. Arguably, this double category is a more fundamental and natural object than the 2-functor $V Cat \to V Prof$. More generally, if $K$ is any 2-category equipped with proarrows, we can reconstruct $K$ and its proarrow equipment from the double category defined above, and we can characterize the double categories that arise in this way. One way to state this characterization is that they are those in which every vertical 1-cell $f\colon A\to B$ has both a [[companion]] (namely $B(1,f)$) and a [[conjoint]] (namely $B(f,1)$). One can then recover $K$ and $M$ as the [[vertical 2-category|vertical and horizontal 2-categories]], respectively, and the 2-functor $K\to M$ as the functor taking every vertical arrow to its companion. Whenever a vertical arrow has both a companion $B(1,f)$ and a conjoint $B(f,1)$, we automatically have an adjunction $B(1,f)\dashv B(f,1)$, so this defines a proarrow equipment in the first sense. Another, perhaps even more natural, way to characterize these double categories is as those with the following property: given any ``niche'' \begin{displaymath} \itexarray{A & & B\\ ^f\downarrow & & \downarrow^g\\ C& \underset{J}{\nrightarrow} & D} \end{displaymath} there exists a ``universal'' or ``cartesian'' filler square \begin{displaymath} \itexarray{A & \overset{J(g,f)}{\to} & B\\ ^f\downarrow & \Downarrow & \downarrow^g\\ C& \underset{J}{\nrightarrow} & D} \end{displaymath} with the property that any other square \begin{displaymath} \itexarray{X & \nrightarrow & Y\\ ^{f h}\downarrow & \Downarrow & \downarrow^{g k}\\ C& \underset{J}{\nrightarrow} & D} \end{displaymath} factors through the universal one uniquely: \begin{displaymath} \itexarray{X & \nrightarrow & Y\\ ^{h}\downarrow & \exists! \Downarrow & \downarrow^{k}\\ A & \overset{J(g,f)}{\to} & B\\ ^f\downarrow & \Downarrow & \downarrow^g\\ C& \underset{J}{\nrightarrow} & D} \end{displaymath} The profunctor $J(g,f)$ will, of course, turn out to be the same one we gave that name to earlier. The proarrows $B(1,f)=U_B(id_B,f)$ and $B(f,1) = U_B(f,id_B)$ are then a special case of this construction. We show that they are a companion and conjoint of $f$, respectively, as follows. By factoring the identity square \begin{displaymath} \itexarray{A & \overset{U_A}{\to} & A\\ ^f\downarrow & ^{U_f}\Downarrow & \downarrow^f\\ B & \underset{U_B}{\to} & B} \end{displaymath} through the universal fillers \begin{displaymath} \itexarray{A & \overset{B(1,f)}{\to} & B\\ ^f\downarrow &\Downarrow & \downarrow^{id}\\ B & \underset{U_B}{\to} & B} \qquad\text{and}\qquad \itexarray{B & \overset{B(f,1)}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f}\\ B & \underset{U_B}{\to} & B} \end{displaymath} that define $B(1,f)$ and $B(f,1)$, we obtain additional squares \begin{displaymath} \itexarray{A & \overset{U_A}{\to} & A\\ ^f\downarrow &\Downarrow & \downarrow^{id}\\ B & \underset{B(f,1)}{\to} & A} \qquad\text{and}\qquad \itexarray{A & \overset{U_A}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f}\\ A & \underset{B(1,f)}{\to} & B} \end{displaymath} such that the composites \begin{displaymath} \itexarray{A & \overset{U_A}{\to} & A\\ ^{f}\downarrow &\Downarrow & \downarrow^{id}\\ B & \overset{B(f,1)}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f}\\ B & \underset{U_B}{\to} & B} \qquad\text{and}\quad \itexarray{A & \overset{U_A}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f}\\ A & \underset{B(1,f)}{\to} & B\\ ^f\downarrow &\Downarrow & \downarrow^{id}\\ B & \underset{U_B}{\to} & B} \end{displaymath} are both equal to $U_f$. And using the uniqueness of factorization through the universal squares, we can conclude moreover that the composites \begin{displaymath} \itexarray{A & \overset{U_A}{\to} & A & \overset{B(1,f)}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f} & \Downarrow & \downarrow^{id}\\ A & \underset{B(1,f)}{\to} & B & \underset{U_B}{\to} & B} \qquad\text{and}\qquad \itexarray{B & \overset{B(f,1)}{\to} & A & \overset{U_A}{\to} & A\\ ^{id}\downarrow &\Downarrow & \downarrow^{f} & \Downarrow & \downarrow^{id}\\ B & \underset{U_B}{\to} & B & \underset{B(f,1)}{\to} & A} \end{displaymath} are equal to the identity squares of $B(1,f)$ and $B(f,1)$ respectively. These are the defining equations of a companion and a conjoint. Finally, we record the following. \begin{lemma} \label{}\hypertarget{}{} There is a natural bijection between squares of the form \begin{displaymath} \itexarray{A_0 & \overset{H}{\to} & B_0\\ ^{f_1}\downarrow && \downarrow^{g_1}\\ A_1 && B_1\\ ^{f_2}\downarrow & \Downarrow & \downarrow^{g_2}\\ A_2 && B_2\\ ^{f_3}\downarrow && \downarrow^{g_3}\\ A_3 & \underset{J}{\to} & B_3 } \end{displaymath} and squares of the form \begin{displaymath} \itexarray{A_1 & \overset{A_1(f_1 ,1)}{\to} & A_0 & \overset{H}{\to} & B_0 & \overset{B_1(1,g_1)}{\to} & B_1\\ ^{f_2}\downarrow && &\Downarrow & && \downarrow^{g_2}\\ A_2 & \underset{A_3(1,f_3)}{\to} & A_3 & \underset{J}{\to} & B_3 & \underset{B_3(g_3 ,1)}{\to} & B_2.} \end{displaymath} \end{lemma} One way to think of this is as saying that vertical arrows can be ``slid around corners'' to become horizontal arrows, turning them into the ``representable proarrows'' $B(1,f)$ or $B(f,1)$ (depending on whether you slid them ``backwards'' or ``forwards'' to get around the corner). The bijection is just given by composing with the four special squares in the definition of companions and conjoints. In particular, by a Yoneda argument, for any $f\colon A\to C$, $g\colon B\to D$, and $J\colon C\nrightarrow D$ we have \begin{equation} J(g,f) \cong C(1,f) \odot J \odot D(g,1) \label{coyon}\end{equation} which was what we took as the the definition of $J(g,f)$ with the original definition of proarrow equipment. Thus, the companions and conjoints determine the rest of the cartesian squares. Note that this is an equipment-version of \href{http://ncatlab.org/nlab/show/Yoneda+reduction}{Yoneda reduction}. In conclusion, we have three definitions of proarrow equipment: \begin{itemize}% \item A 2-functor which is bijective on objects, locally fully faithful, and maps every 1-morphism to one having a right adjoint. \item A double category in which every vertical arrow has a companion and a conjoint. \item A double category in which every niche has a cartesian filler. \end{itemize} While the first definition is perhaps simpler, for some purposes the second and third definitions are preferable. For instance, the definition of the 3-category of ``2-categories equipped with proarrows'' is much more naturally defined by viewing them as double categories. (See Dominic Verity's thesis and Mike Shulman's paper on framed bicategories.) It also generalizes better to situations in which not all proarrows have composites; see ``virtual equipments,'' below. \hypertarget{as_a_category_internal_to_}{}\subsubsection*{{As a category internal to $Cat$}}\label{as_a_category_internal_to_} We discuss how a 2-category with proarrow equipment is an [[internal category]] in the [[(2,1)-category]] [[Cat]] in the sense of the theory of \emph{[[internal (∞,1)-categories]]}. (\ldots{}) For the moment see at \emph{\href{http://ncatlab.org/nlab/show/Segal%20space#ExamplesInIGrpd}{Segal space - Examples - In 1Grpd}}. \hypertarget{related_notions}{}\subsubsection*{{Related notions}}\label{related_notions} There are a number of variations on the notion. \begin{itemize}% \item [[virtual proarrow equipment]] \item [[1-category proarrow equipment]] \item [[(1,2)-category proarrow equipment]] \end{itemize} Some related concepts include: \begin{itemize}% \item [[cartesian bicategory]] \item [[bicategory of relations]] \item [[allegory]] \end{itemize} See also at [[Segal space]], the section \emph{\href{Segal+space#ExamplesInIGrpd}{Examples -- In 1Grpd}}. \hypertarget{category_theory_in_a_proarrow_equipment}{}\subsection*{{Category theory in a proarrow equipment}}\label{category_theory_in_a_proarrow_equipment} We now give a few examples of how to do category theory internal to a proarrow equipment. \hypertarget{HomsetAdjn}{}\subsubsection*{{Homset definition of adjunctions}}\label{HomsetAdjn} We start with this: two (vertical) arrows $f\colon A\to B$ and $g\colon B\to A$ are adjoint (in $\mathcal{V}(\underline{X})$) if and only if we have an isomorphism $B(f,1)\cong A(1,g)$. Why? Well, an adjunction $f\dashv g$ comes with a unit and a counit, which (expressed in $\underline{X}$) are of the form \begin{displaymath} \itexarray{A & \overset{U_A}{\to} & A\\ ^f\downarrow && \downarrow\\ B & \overset{\eta}{\Leftarrow} & \downarrow^{id} \\ ^g\downarrow && \downarrow\\ A& \underset{U_A}{\to} & A} \qquad\text{and}\qquad \itexarray{B & \overset{U_B}{\to} & B\\ \downarrow && \downarrow^g\\ ^{id}\downarrow & \overset{\varepsilon}{\Leftarrow} & A \\ \downarrow && \downarrow^f\\ B& \underset{U_B}{\to} & B.} \end{displaymath} Applying the bijection of the Central Lemma, we see that $\eta$ corresponds to a map $B(f,1) \to A(1,g)$, and likewise $\varepsilon$ corresponds to a map $A(1,g)\to B(f,1)$. The triangle identities for $\eta$ and $\varepsilon$ are then equivalent to saying that these two maps are inverse isomorphisms. So we've recovered the classical equivalence between the ``diagrammatic'' and isomorphism-of-hom-sets definitions of an adjunction, in a purely formal way. \hypertarget{fully_faithful_arrows}{}\subsubsection*{{Fully faithful arrows}}\label{fully_faithful_arrows} An arrow $f:A\to B$ in a 2-category equipped with proarrows is said to be \textbf{fully faithful} if the canonical morphism $U_A\to B(f,f)$ is an isomorphism of proarrows $A\to A$. In $V Cat$ this recaptures the correct notion of $V$-fully-faithful $V$-functor. It is not hard to see, using the fact that $K\to M$ is locally fully faithful, that any fully-faithful arrow $f\colon A\to B$ is, in fact, internally fully-faithful in $K$ in the sense that $K(X,A)\to K(X,B)$ is fully faithful for all $X\in K$. However, the converse fails in general. But it is not hard to show that the two are equivalent if $f\colon A\to B$ has a left or right adjoint, using the above characterization of adjunctions. \hypertarget{limits}{}\subsubsection*{{Limits}}\label{limits} The notion of limit we end up in a 2-category equipped with prarrows with is actually more general than what you're probably used to, but this extra generality turns out to be useful. Let $d\colon D\to C$ be an arrow and let $J\colon D\nrightarrow A$ be a proarrow; we're going to define what it means for an arrow $\ell\colon A\to C$ to be the \emph{$J$-weighted limit} of $d$. In the proarrow-equipped 2-category $V Cat$ of $V$-enriched categories, if $A$ is the \href{http://ncatlab.org/nlab/show/unit+enriched+category}{unit} $V$-category $I$, then this will recover the usual notion of \href{http://ncatlab.org/nlab/show/weighted+limit}{weighted limit}. Of course, in a general proarrow equipment we may not have a ``unit object,'' so that extra generality is unavoidable; it's like using generalized elements in ordinary category theory. To make things easier, let's assume that our proarrow equipment is \emph{closed}, in the sense that composition of proarrows has adjoints in each variable \begin{displaymath} \mathcal{H}(\underline{X})(H\odot K,L) \cong \mathcal{H}(\underline{X})(H,K\rhd L) \cong \mathcal{H}(\underline{X})(K,L\lhd H). \end{displaymath} The Central Lemma implies that analogously to \eqref{coyon}, we have \begin{equation} K(g,f) \cong D(1,g)\rhd K \lhd C(f,1). \label{yon}\end{equation} In $V\text{-}Prof$, the adjoints are given by the \href{http://ncatlab.org/nlab/show/end}{ends} \begin{displaymath} (K\rhd L)(b,a) = \int_{c\in C} [K(c,b), L(c,a)] \end{displaymath} and \begin{displaymath} (L \lhd H)(c,b) = \int_{a\in A} [H(b,a), L(c,a)]. \end{displaymath} Therefore, \eqref{yon} is an abstract form of the Yoneda lemma, just as \eqref{coyon} is an abstract form of Yoneda reduction. Now recall that for $V$-categories $D$ and $C$, an object $\ell\in C$ is a $J$-weighted limit of $d\colon D\to C$ if we have a natural isomorphism \begin{displaymath} \begin{aligned} C(c,\ell) &\cong [D,V](J, C(c,d(-)))\\ &= \int_{x\in D} [J(x), C(c,d(x))]. \end{aligned} \end{displaymath} Thus it makes sense to define, in a closed proarrow equipment, an arrow $\ell\colon A\to C$ to be the $J$-weighted limit of $d$ if we have an isomorphism \begin{displaymath} C(1,\ell) \cong C(1,d) \lhd J. \end{displaymath} (If our proarrow equipment is not closed, we simply assert that $C(1,\ell)$ has the universal property that $C(1,d) \lhd J$ would have if it existed. In other terminology, we assert that $C(1,\ell)$ is a \emph{right lifting} of $C(1,d)$ along $J$ in the 2-category of proarrows.) In particular, when $A$ is the unit $V$-category, this recovers the classical notion. But even in $V Cat$ there are interesting examples for other values of $A$. If we take $J = D(j,1)$ for some functor $j\colon A\to D$, then \eqref{coyon} and \eqref{yon} imply that \begin{displaymath} \begin{aligned} C(1,d) \lhd J &= C(1,d) \lhd D(j,1)\\ & \cong j^* C(1,d)\\ & \cong D(1,j) \odot C(1,d)\\ & \cong C(1,d j) \end{aligned} \end{displaymath} so that $\ell = d j$ is the $J$-weighted limit of $d$. That is, $D(j,1)$-weighted limits are just given by composition with $j$. More interestingly, one can show that if $J = D(1,k)$ for some $k\colon D\to A$, then $J$-weighted limits specialize to \emph{pointwise} right Kan extensions along $k$. That is, the extra data of a proarrow equipment lets us define the good notion of Kan extension (even in the enriched case) as a special case of a general notion of limit. Thus, in a general 2-category equipped with proarrows, we \emph{define} a ``pointwise right Kan extension'' along an arrow $k\colon D\to A$ to be a $D(1,k)$-weighted limit. It is easy to show that any pointwise Kan extension is, in particular, an internal Kan extension in $K$, but as we have seen the converse fails in $V Cat$. \hypertarget{right_adjoints_preserve_limits}{}\subsubsection*{{Right adjoints preserve limits}}\label{right_adjoints_preserve_limits} Suppose that $\ell\colon A\to C$ is a $J$-weighted limit of $d\colon D\to C$ in the above sense, and let $g\colon C\to B$ be an arrow with a left adjoint $f\colon B\to C$. We want to show that $g\ell$ is a $J$-weighted limit of $g d$. But we have \begin{displaymath} \begin{aligned} B(1,g\ell) &\cong C(1,\ell) \odot B(1,g)\\ &\cong \big(C(1,d) \lhd J\big) \odot C(f,1)\\ &\cong C(1,f) \rhd \big(C(1,d) \lhd J\big)\\ &\cong \big(C(1,f) \rhd C(1,d)\big) \lhd J\\ &\cong \big(C(1,d) \odot C(f,1)\big) \lhd J\\ &\cong \big(C(1,d) \odot B(1,g)\big) \lhd J\\ &\cong B(1,g d) \lhd J. \end{aligned} \end{displaymath} which is what we want. \hypertarget{graphs_and_cographs}{}\subsection*{{Graphs and cographs}}\label{graphs_and_cographs} As noted above, in the case of ordinary categories, the profunctors can in fact be recovered from the 2-category $Cat$. Specifically, profunctors $A\to B$ can be identified with two-sided discrete fibrations from $B$ to $A$ (that is, spans $B \leftarrow C \to A$ such that $C \to B$ is a [[Grothendieck fibration|(Grothendieck) fibration]], $C\to A$ is an opfibration, the two structures are compatible, and each fiber of $C\to B\times A$ is discrete). The two-sided fibration corresponding to a profunctor is also called its [[graph of a profunctor|graph]]. The same is true for internal categories, but not for enriched categories. However the $V$-profunctors $A\to B$ \emph{can} be recovered from the 2-category $V Cat$ in a different, and in fact dual, way: they are the two-sided [[codiscrete cofibrations]] from $B$ to $A$, i.e. two-sided discrete fibrations in $(V Cat)^{op}$. The two-sided cofibration corresponding to a profunctor is, unsurprisingly, its [[cograph of a profunctor|cograph]], and also its [[collage]]. This was first noticed by Street and subsequently expanded on by other authors. In particular, one can write down axioms on a 2-category guaranteeing that its codiscrete cofibrations can be used to equip it with proarrows, and axioms on a proarrow equipment guaranteeing that it arises from codiscrete cofibrations. \hypertarget{virtual_equipments}{}\subsection*{{Virtual equipments}}\label{virtual_equipments} One can formulate a generalized notion of equipment which includes $V Cat$ for \emph{any} monoidal category $V$ (and in fact, any [[multicategory]]), and $Cat(S)$ for any category $S$ with pullbacks. The precise definition is complicated, but the basic idea is not: we start from the double-category definition, and instead of composites of the horizontal (pro)arrows, we allow the squares to have domains that are arbitrary composable strings, like so: \begin{displaymath} \itexarray{ & \to \to \dots \to &\\ \downarrow & \Downarrow & \downarrow\\ & \underset{}{\to}& .} \end{displaymath} So far this is analogous to the generalization from monoidal categories to multicategories, and gives the notion of [[virtual double category]]. We then impose a condition analogous to the existence of companions and conjoints to obtain the notion of [[virtual equipment]]. Most of category theory can be done in a virtual equipment just as well as in an equipment. \hypertarget{CategoriesEnrichedInAnEquipment}{}\subsection*{{Categories enriched in an equipment}}\label{CategoriesEnrichedInAnEquipment} For any equipment $W$ one can define a notion of \textbf{$W$-enriched category}. (See also at \emph{[[category enriched in a bicategory]]}.) This consists of \begin{itemize}% \item a collection $ob(C)$ of objects, \item for each object $x$ an \emph{extent} $e(x)$ which is an object of $W$, \item for each pair of objects $x,y$ a proarrow $hom_C(x,y):e(x)\to e(y)$, \item composition and identity-assigning 2-cells obeying associativity and unit axioms. \end{itemize} So far we have not used the ordinary arrows, so many authors have studied only the notion of ``category enriched in a bicategory.'' (Note that any 2-category $M$ can be regarded as the proarrow 2-category of an equipment in which the only ordinary arrows are identites.) However, we need the extra structure when we define a \emph{functor} $f:C\to D$ between $W$-enriched categories, which consists of: \begin{itemize}% \item a function $f:ob(C)\to ob(D)$, \item for each object $x$ of $C$ an arrow $f_x:e(x)\to e(f(x))$ in $W$, \item for each pair of objects $x$ and $y$, a square\begin{displaymath} \itexarray{e(y) & \overset{hom_C(x,y)}{\to} & e(x)\\ ^{f_y}\downarrow & \Downarrow & \downarrow^{f_x}\\ e(f(y))& \underset{hom_D(f(x),f(y))}{\to} & e(f(x))} \end{displaymath} \item satisfying functoriality axioms. \end{itemize} Finally, we define a \emph{natural transformation} between such functors $f,g:C\to D$ to consist of \begin{itemize}% \item squares\begin{displaymath} \itexarray{e(x) & \overset{U_{e(x)}}{\to} & e(x)\\ ^{g_x}\downarrow & \Downarrow & \downarrow^{f_x}\\ e(g(x))& \underset{hom_D(f(x),f(y))}{\to} & e(f(x))} \end{displaymath} \item satisfying a naturality axiom. \end{itemize} By choosing $W$ appropriately, categories enriched in an equipment include most types of generalized category: \begin{itemize}% \item If $W$ is a monoidal category $V$, regarded as a one-object bicategory and thence as an equipment with only one ordinary arrow (so the objects of $V$ are the proarrows of $W$), then $W$-enriched categories, functors, and natural transformations are the same as $V$-enriched ones. \item If $S$ has pullbacks, there is an equipment $Span(S)$ whose objects and arrows are those of $S$ and whose proarrows are spans. A category enriched in $Span(S)$ which has one object is the same as an internal category in $S$, and likewise for functors and transformations. (Here it is essential to use an equipment, rather than merely a bicategory, to get the right notion of functor.) \item Arbitrary $Span(S)$-enriched categories can be identified with ``locally small fibrations'' over $S$, aka ``locally internal categories'' over $S$. \end{itemize} Other choices of $W$ give ``categories which are both enriched and internal,'' for example: \begin{itemize}% \item For a suitably nice category $S$ (such as a [[Grothendieck topos]]) there is an equipment $Ab(S)$ whose objects and arrows are those of $S$, and whose proarrows $A\to B$ are internal abelian group objects in $S/(B\times A)$. An $Ab(S)$-enriched category with one object can be regarded as an ``internal [[Ab-enriched category]]'' in $S$. \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item R.J. Wood, ``Abstract Proarrows I'' and ``Proarrows II'' (the original definitions), and a number of following papers. \item [[Ross Street]], ``Fibrations in bicategories'' (Construction of $V Mod$ from $V Cat$.) \item [[Aurelio Carboni]], Scott Johnson, [[Ross Street]], and [[Dominic Verity]], ``Modulated bicategories'' (Improved construction of $V Mod$ from $V Cat$.) \item [[Dominic Verity]], ``Enriched categories, internal categories, and change of base'', Ph.D. Thesis. (The connection with double categories.) \item [[Michael Shulman]], ``Framed bicategories and monoidal fibrations''. (The equivalence with certain double categories, there called \emph{framed bicategories}, and a general way to construct equipments such as $Ab(S)$.) \item [[Geoff Cruttwell]], [[Michael Shulman]], ``A unified framework for generalized multicategories'' (currently the only reference for virtual equipments). \item Renato Betti, [[Aurelio Carboni]], [[Ross Street]], and Robert Walters, ``Variation through enrichment.'' (Locally small fibrations as $Span$-enriched categories.) \end{itemize} A blog post surveying ideas of proarrow equipments, much of which has been copied over to this page: \begin{itemize}% \item [[Mike Shulman]], \emph{Equipments} (\href{http://golem.ph.utexas.edu/category/2009/11/equipments.html}{blog}) \end{itemize} [[!redirects 2-category equipped with proarrows]] [[!redirects 2-categories equipped with proarrows]] [[!redirects 2-category equipped with pro-arrows]] [[!redirects 2-categories equipped with pro-arrows]] [[!redirects 2-category with proarrow equipment]] [[!redirects 2-categories with proarrow equipment]] [[!redirects 2-category with pro-arrow equipment]] [[!redirects 2-categories with pro-arrow equipment]] [[!redirects 2-category equipment]] [[!redirects 2-category equipments]] [[!redirects equipment]] [[!redirects equipments]] [[!redirects proarrow equipment]] [[!redirects proarrow equipments]] [[!redirects pro-arrow equipment]] [[!redirects pro-arrow equipments]] [[!redirects proarrow]] [[!redirects proarrows]] \end{document}