2adjoint.tex

\documentclass{amsart}
\usepackage{mathpartir,mathtools,amssymb}
\usepackage[all]{xy}
\def\flet#1:=^#2#3in{\mathsf{let}\;#1 \coloneqq^{#2} #3\;\mathsf{in}\;}
\def\type{\mathsf{type}}
\def\lax{\sim\hspace{-5pt}:\hspace{3pt}}
\def\inr{\mathsf{inr}\;}
\def\inl{\mathsf{inl}\;}
\def\case{\mathsf{case}}
\def\refl{\mathsf{refl}}
\def\J{\mathcal{J}}
\def\K{\ensuremath{\mathcal{K}}}
\def\I{\ensuremath{\mathbb{I}}}
\def\O{\ensuremath{\mathbb{O}}}
\def\ctx{\:\mathsf{ctx}}
\def\finset{\mathrm{FinSet}}
\let\ot\leftarrow
\def\sem{\mathsf{Sem}}
\def\el{\mathrm{el}}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{claim}{Claim}
\title{Thoughts on adjoint logic indexed by a 2-category}
\begin{document}
\maketitle

\section{Indexing of contexts and judgments}
\label{sec:indexing-contexts}

Let \K\ be the 2-category of modes.
I will write $\alpha^* \dashv \alpha_*$ for the adjunction $F_\alpha \dashv U_\alpha$, since I'm thinking of it as a geometric morphism.
The variance is that if $\mu:\alpha\to\beta$ is a 2-cell, then we have $\beta^* \to \alpha^*$ and $\alpha_* \to \beta_*$ (which are mates).
Semantics will occur relative to some pseudofunctor $\sem:\K\to\mathrm{Adj}$.

Let's think about what data in \K\ should parametrize a judgment with multiple hypotheses and dependent types.
The simple case is when $\alpha:y\to x$ and we have only one hypothesis:
\[ x:A_x \vdash_{\alpha} b : B_y \]
Semantically, this is a map $\alpha^*A_x \to B_y$ in $\sem(y)$, or equivalently $A_x \to \alpha_* B_y$ in $\sem(x)$.
But the same rule should apply to dependent types, since they are maps into the universe:
\[ x:A_x \vdash_{\alpha} B_y : \type_y \]
Semantically, a judgment like this means that $B_y$ is a fibration over $\alpha^* A_x$.

Now we should be able to add a variable of this type to the context:
\[ x:A_x , y:B_y \vdash \]
which means that in a context we must somehow keep track of morphisms relating the modes at which the variables live.
A term in this context
\[ x:A_x , y:B_y \vdash c : C_z\]
ought to involve morphisms $\beta : z \to y$ and $\gamma: z\to x$, which are related in some way to $\alpha$.
It seems to me that the correct relationship is a 2-cell $\mu : \alpha \beta \to \gamma$.
This allows us to say semantically that this is a map to $C_z$ from the following pullback:
\begin{equation*}
  \vcenter{\xymatrix{
      \bullet \ar[r]\ar[d] &
      \beta^* B_y\ar[d]\\
      \gamma^* A_x \ar[r] &
      \beta^* \alpha^* A_x
      }}
\end{equation*}
Similarly, a dependent type
\[ x:A_x , y:B_y \vdash C_z :\type_z\]
will be a fibration over this pullback, and so when we add it to the context, we have to record not only $\alpha$, $\beta$, and $\gamma$, but also $\mu$.

However, there is also no reason that dependence must proceed linearly, and when there are multiple modes we cannot simply weaken the dependence.
For instance, if in addition to $\alpha:y\to x$ we have $\delta : w\to x$, and dependent types
\[ x:A_x \vdash_{\alpha} B_y : \type_y \]
\[ x:A_x \vdash_{\delta} D_w : \type_w \]
then we should be able to add them both to the context, without needing to factor one of them through the other even laxly:
\begin{equation}
  x:A_x, y:B_y, w:D_w \vdash\label{eq:abd-context}
\end{equation}
so that this context must keep track of $\alpha$ and $\delta$ both.
Now a term in this context
\[ x:A_x, y:B_y, w:D_w \vdash c:C_z \]
ought to involve morphisms $\beta : z\to y$ and $\gamma : z \to x$ and $\phi : z\to w$ related in some way.
It seems that the right relationship is a pair of 2-cells $\mu: \gamma \to \alpha\beta$ and $\nu: \gamma \to \delta\phi$, so that this term is a map to $C_z$ from the following combined pullback:
\[ \xymatrix{
  && \bullet \ar[dl] \ar[dr] \\
  \phi^* D_w \ar[d] & \bullet \ar[dr] \ar[l] && \bullet\ar[dl] \ar[r] & \beta^* B_y \ar[d] \\
  \phi^* \delta^* A_x && \gamma^*A_x \ar[ll]^{\nu^*} \ar[rr]_{\mu^*} && \beta^* \alpha^* A_x }
\]

In general, we should allow any reasonable sort of dependency within a context.
A convenient way to formalize this is by indexing contexts, not by natural numbers, but by \emph{finite inverse categories}.
The ordinary sort of context, in which each type depends on all the previous ones, correspond to ``linear'' inverse categories
\[\ot\ot\ot\cdots\ot,\]
while the context~\eqref{eq:abd-context} above will correspond instead to the inverse category $\to\ot$.

Since we must assign a mode to every type, we ought to additionally have some sort of functor from our finite inverse category to the category of modes.
The presence of the 2-cells such as $\mu$ and $\nu$ suggests that this should be a \emph{lax} functor.
Since we don't need identity comparison 2-cells, we should make it a \emph{normal lax functor}.

\begin{claim}
  Contexts in 2-adjoint logic should be indexed by pairs $(\I,\Phi)$, where \I\ is a finite inverse category and $\Phi : \I \to \K$ is a normal lax functor from \I\ to the 2-category \K\ of modes.
  We may write such a context as
  \[ \Gamma \ctx_{\I,\Phi}. \]
\end{claim}

In what follows, I will probably sometimes be imprecise by omitting to notate the functor $\Phi$, i.e.\ failing to distinguish between objects and morphsims in $\I$ and their images in $\K$.

Above we described the intended semantic meaning of this in terms of maps out of pullbacks, when the maps are into the universe, they are equivalently fibrations \emph{into} the pullback, and thus the pullback object can be dispensed with by invoking its universal property.
Thus, for instance, a context such as
\[ x:A_x , y:B_y , z: C_z \vdash\]
indexed by $\alpha:y\to x$, $\beta:z\to y$, $\gamma:z\to x$, and $\mu:\alpha\beta\to\gamma$ consists of objects $A_x$, $B_y$, and $C_z$ in modes $x$, $y$, and $z$ respectively, a map $B_y \to \alpha^* A_x$, and maps $C_z \to \beta^*B_y$ and $C_z \to \gamma^*A_x$ forming a commutative square
\begin{equation*}
  \vcenter{\xymatrix{
      C_z \ar[r]\ar[d] &
      \beta^* B_y\ar[d]\\
      \gamma^* A_x \ar[r]_{\mu^*} &
      \beta^* \alpha^* A_x.
      }}
\end{equation*}
Thinking about a few more examples leads to the following conclusion:

\begin{claim}
  The semantic correspondent of $\Gamma \ctx_{\I,\Phi}$ is an object of the \emph{oplax limit} of $\Phi$.
  More specifically, it consists of an object $A_x \in \sem(x)$ for each object $x\in \I$ and a morphism (fibration) $A_y \to \alpha^* A_x$ in $\sem(y)$ for each morphism $\alpha:y\to x$ in $\I$, such that for any composable pair $z \xrightarrow{\beta} y\xrightarrow{\alpha} x$ in $\I$ the following square commutes:
  \begin{equation*}
    \vcenter{\xymatrix{
        A_z \ar[r]\ar[d] &
        \beta^* A_y\ar[d]\\
        (\alpha\beta)^* A_x \ar[r] &
        \beta^* \alpha^* A_x.
      }}
  \end{equation*}
\end{claim}

Now, since a type in some context can always be added to that context, types and terms in context $\Gamma \ctx_{\I,\Phi}$ should be indexed by a pair $(\I',\Phi')$ that extends $(\I,\Phi)$ with one additional object ``at the top'', i.e.\ one which receives no arrows from any object in \I.
Such a finite inverse category $\I'$ is uniquely specified by a functor $H:\I\to\finset$ (the covariant hom-functor of the new object), in which case $\I'$ is the ``collage'' or ``gluing'' of this functor; let us denote it $\I\oplus H$.
Given this, to extend $\Phi:\I\to\K$ to $\Phi':\I'\to\K$ is to give an object $h\in\K$ together with a lax natural transformation $\theta : H \to \K(h,\Phi)$.
Thus, we write $\Phi' = \Phi \oplus (h,\theta)$.

\begin{claim}
  Type and term judgments in 2-adjoint logic should be indexed by quintpules $(\I,\Phi,H,h,\theta)$ as above.
  We might write such a judgment as
  \[ \Gamma\vdash_{\I,\Phi}^{H,h,\theta} \J \]
\end{claim}

I am not claiming that for a given 2-category of modes \K, \emph{all} such quintuples must be used to index judgments; only the converse that each judgment is indexed by some quintuple.
For particular values of \K\ it will probably (hopefully!)\ be the case that choosing only a few such quintuples suffices to give a useful theory.
However, for purposes of general theory, we ought to allow any quintuples.

To define the meaning of this semantically, given $(\I,\Phi,H,h,\theta)$ and a context $\Gamma\ctx_{\I,\Phi}$ (consisting of objects $\Gamma_x$ and morphisms $\Gamma_\alpha : \Gamma_y \to \alpha^*\Gamma_x$), we can define an object $\theta^*\Gamma \in \sem(h)$ as follows.
Recall that $\el(H)$ denotes the category of elements of $H$, whose objects are pairs $(x,\beta)$ where $\beta\in H(x)$, and whose morphisms $(x,\beta)\to (x',\beta')$ are morphisms $\gamma :x\to x'$ in $\I$ such that $H(\gamma)(\beta) = \beta'$.
We let $\theta^*\Gamma$ be the equalizer of the following pair of maps:
\[ \xymatrix@C=3pc{\displaystyle\prod_{(x,\beta)\in\el(H)} \theta_\beta^*(\Gamma_x)
  \ar@<2mm>[r]^-{\mathrm{lax}_\theta} \ar@<-2mm>[r]_-{\theta_\beta^*(\Gamma_\gamma)} &
  \displaystyle\prod_{\gamma : (x,\beta)\to (x',\beta')} \theta_\beta^*(\gamma^* \Gamma_{x'})} \] 
This is morally a sort of ``end'' over the category $\el(H)$, but I don't think it can literally be described as an end of the usual sort.
But like an end, it \emph{should} alternatively be expressable as a limit over the ``twisted arrow category'' of $\el(H)$.

Of course, in general not all limits may exist in the category $\sem(h)$.
But I expect it should be possible to prove inductively that this particular limit exists, assuming the appropriate fibrancy conditions on $\Gamma$ and the functors involved and the fact that pullbacks of fibrations exist.

\begin{claim}
  The semantic meaning of a judgment $\Gamma\vdash_{\I,\Phi}^{H,h,\theta} B:\type$ is a fibration over $\theta^*\Gamma$ in $\sem(h)$.
  Given such a $B$, the semantic meaning of $\Gamma\vdash_{\I,\Phi}^{H,h,\theta} b:B$ is a section of this fibration.
\end{claim}

To justify this somewhat, note that a map into $\theta^*\Gamma$, with domain $\Gamma_h$ say, is, by the universal property of the equalizer, determined by maps $\Gamma_{\beta} : \Gamma_h \to \Gamma_x$ for all $\beta\in H(x)$ such that the following square commutes for any ${\gamma : (x,\beta)\to (x',\beta')}$ in $\el(H)$:
\begin{equation*}
  \vcenter{\xymatrix{
      \Gamma_h \ar[r]\ar[d] &
      \theta_\beta^* \Gamma_y\ar[d]\\
      \theta_{\beta'}^* \Gamma_x \ar[r] &
      \theta_\beta^* \gamma^* \Gamma_x.
    }}
\end{equation*}
But this is precisely what is needed to extend our object $\Gamma$ of the oplax limit of $\Phi$ to an object of the oplax limit of $\Phi \oplus (h,\theta)$.
Thus, a type in context $\Gamma$ can always be added to the context, so our semantic notions are at least consistent (modulo the issue of fibrancy, which remains to be considered).

As a simple example, suppose that $\I$ is a discrete category, with no nonidentity arrows, and that $H$ is constant at $\mathbf{1}$.
This means there is no dependence at all between types in the context, but types and terms can depend uniquely on every variable in the context.
In this case, $\theta^* \Gamma$ reduces to
\[ \prod_{x\in \I} \theta_{\star}^* \Gamma_x \]
and so we are talking about fibrations over this product and sections of those.
When the type dependency of the target is likewise trivial, we are simply talking about maps out of this product, which seems right.

Note that our enhanced contexts are able to sort of ``record weakening and contraction''.
If $H(h,i)=\emptyset$ for some $i$, then our judgment doesn't actually depend on $A_i$ at all, while if $H(h,i)$ has more than one element, our judgment actually depends on two or more copies of $A_i$.

\section{Context morphisms and substitution}
\label{sec:substitution}

Now that we have many different sorts of contexts, it becomes trickier to say what is meant by substitution.
In particular, we need to say what is a ``context morphism'' between two contexts indexed by different diagrams.
I think it should be possible to do this with profunctors and a sort of half-lax diagram indexed by them.
(TODO\dots)


% \section{The adjoint connectives}
% \label{sec:adjoint-connectives}

% For now, let's think about the rules for the adjoint connectives $\alpha^*$ and $\alpha_*$.
% The easiest one is UR:
% \[ \inferrule{\Gamma \vdash_{\O \circ \beta} M : A}{\Gamma \vdash_{\O} M_\beta : \beta_* B} \]
% Here $\O$ is an oriental ending at a mode $p_{n}$, and $\beta$ is a morphism $y \to p_{n}$, so that we have an oriental $\O \circ \beta$ obtained by composing each morphism $\alpha_{ni}$ with $\beta$.
% To see that this is sensible, think about the non-dependent semantics: the hypothesis is a map
% \[ (\alpha_{n1}\beta)^* A_1 \times \cdots \times (\alpha_{n,n-1}\beta)^* A_{n-1} \longrightarrow B \]
% which, assuming $\beta^*$ preserves products, is equivalent to a map
% \[ \beta^*\Big(\alpha_{n1}^* A_1 \times \cdots \times \alpha_{n,n-1}^* A_{n-1}\Big) \longrightarrow B \]
% and hence to a map
% \[ \alpha_{n1}^* A_1 \times \cdots \times \alpha_{n,n-1}^* A_{n-1} \longrightarrow \beta_* B \]
% which is the conclusion.

% For UL, note that any $n$-oriental $\O$ contains $n$ $(n-1)$-orientals $\partial_i\O$ obtained by omitting the mode $p_i$.
% Now let $\O$ be an $(n+1)$-oriental such that $\alpha_{n,n-1} = \beta$; then the rule is
% \[ \inferrule{\Gamma,u:A \vdash_{\partial_{n-1} \O} M:B}{\Gamma,x:\beta_*A \vdash_{\partial_n \O} (\flet u_\beta :=^\O x in M):B} \]
% Note that the oriental $\O$ can be considered extra data chosen on $\partial_{n}\O$ and $\beta$.
% So we can read this rule backwards as: given an arbitrary $n$-oriental ``$\partial_{n}\O$'' and a morphism $\beta$ ending at $p_{n-1}$, we can construct an element of $B$ judged along $\partial_{n}\O$ with a last hypothesis in $\beta_*A$ by choosing an $(n+1)$-oriental extending $\partial_{n}\O$ and $\beta$ and giving an element of $B$ judged along $\partial_{n-1}\O$ whose last hypothesis is instead in $A$.
% Semantically (and non-dependently), the hypothesis is a map
% \[ \alpha_{n+1,\bullet}^*\Gamma \times \alpha_{n+1,n}^* A \longrightarrow B \]
% and since $\beta = \alpha_{n,n-1}$, we have a natural transformation
% \[ \alpha_{n+1,n-1}^* \beta_* \to \alpha_{n+1,n}^* \beta^* \beta_*  \to \alpha_{n+1,n}^* \]
% using $\mu_{n+1,n,n-1}$ and the counit of the adjunction $\beta^* \dashv \beta_*$.
% Thus, we can compose with this transformation at $A$ to obtain the conclusion:
% \[ \alpha_{n+1,\bullet}^*\Gamma \times \alpha_{n+1,n-1}^* \beta_* A \longrightarrow B. \]

% The rule FL is similar, but with an extra condition.
% Let $\O$ be an $(n+1)$-oriental such that $\alpha_{n,n-1} = \beta$, and moreover $\mu_{n+1,n,n-1}$ is an identity (or an isomorphism).
% Then the rule is
% \[ \inferrule{\Gamma,u:A \vdash_{\partial_{n} \O} M:B}{\Gamma,x:\beta^* A \vdash_{\partial_{n-1} \O} (\flet u^\beta :=^\O x in M):B} \]
% Again, the rule can be read backwards by considering $\O$ as extra data chosen on $\partial_{n-1}\O$ and $\beta$.
% Semantically and non-dependently, the hypothesis is a map
% \[ \alpha_{n+1,\bullet}^*\Gamma \times \alpha_{n+1,n-1}^* A \longrightarrow B \]
% But since $\alpha_{n+1,n-1} \cong \beta \alpha_{n+1,n}$ (the isomorphism $\mu_{n+1,n,n-1}$), this is equivalent to a map
% \[ \alpha_{n+1,\bullet}^*\Gamma \times \alpha_{n+1,n}^* \beta^* A \longrightarrow B \]
% which is the conclusion.

% (Is the fact that the hypotheses of UR and FL are \emph{equivalent} to their conclusions what Reed meeds by saying that U is invertible on the right and F is invertible on the left?)

% I would like to also have ``Frobenius-ified'' versions of UL and FL that apply to a hypothesis anywhere in the context instead of just at the end.
% I'm not sure whether that is easy or not.

% Finally, FR is the trickiest.
% Here's the best I've been able to come up with; I'm not positive it's correct.
% Let $\O$ be an $(n+1)$-oriental and $1\le k\le n$, with $\alpha_{n+1,k} = \beta$.
% Then in addition to the $n$-oriental $\partial_k \O$, we have a $k$-oriental $\partial_{\le k} \O$ obtained by discarding all modes after $p_k$.
% Now the rule is
% \[ \inferrule{\Gamma\!\downharpoonright_k\; \vdash_{\partial_{\le k}\O} M : B }{\Gamma \vdash_{\partial_k \O} M^\beta : \beta^* B} \]
% Here $\Gamma\!\downharpoonright_k$ denotes $\Gamma$ restricted to $\partial_{< k}\O$.
% Semantically and non-dependently, the hypothesis is a map
% \[ \alpha_{k1}^* A_1 \times \cdots \times \alpha_{k,k-1}^* A_{k-1} \longrightarrow B \]
% so we can obtain the conclusion as the composite
% \begin{align*}
%   (\alpha_{n+1,1})^* A_1 \times \overbrace{\cdots}^{\widehat{k}} \times (\alpha_{n+1,n})^* A_{n}
%   &\to (\alpha_{n+1,1})^* A_1 \times {\cdots} \times (\alpha_{n+1,k-1})^* A_{k-1}\\
%   % &\to (\alpha_{k1}\alpha_{n+1,k})^* A_1 \times {\cdots} \times (\alpha_{k,k-1}\alpha_{n+1,k})^* A_{k-1}\\
%   &\to (\alpha_{k1}\beta)^* A_1 \times \cdots \times (\alpha_{k,k-1}\beta)^* A_{k-1}\\
%   &\cong \beta^*\alpha_{k1}^* A_1 \times \cdots \times \beta^*\alpha_{k,k-1}^* A_{k-1}\\
%   &\cong \beta^*\Big(\alpha_{k1}^* A_1 \times \cdots \times \alpha_{k,k-1}^* A_{k-1} \Big)\\
%   &\to \beta^* B.
% \end{align*}
% where the noninvertible maps are respectively a projection, induced by the 2-cells $\mu_{n+1,k,i}$, and the hypothesis.

% There should be computation rules that involve information about composition in \K.


% \section{Flat and sharp}
% \label{sec:flat-sharp}

% Now let's specialize to the case when $\K$ is the walking coreflection.
% Thus, it has two modes $v$ and $t$, two generating morphisms $\delta:t\to v$ and $\gamma:v\to t$, such that $\delta\gamma = 1_v$ (hence $\gamma\delta$ is idempotent), and a 2-cell $\epsilon : \gamma\delta \to 1_t$ such that $\delta*_l\epsilon$ and $\epsilon*_r\gamma$ are identities.

% An $n$-oriental in this \K\ is determined by the following:
% \begin{itemize}
% \item A list $p_1,\dots,p_n$ of modes (i.e.\ each either $v$ or $t$).
% \item Whenever $i<j$ and $p_i = p_j = t$, a choice of either $1_t$ or $\gamma\delta$ to be $\alpha_{ji}$.
%   (All other hom-sets are uniquely inhabited.)
% \item Whenever $i<j<k$ and $p_i = p_k = t$ and $\alpha_{ki} = 1_t$, it must be the case that $p_j = t$ and $\alpha_{kj} = \alpha_{ji} = 1_t$ as well.
%   (Any 2-cell other than $1_t$ is initial in its hom-category, so there is a unique choice of $\mu$.)
% \end{itemize}
% In particular, when making a judgment whose conclusion has mode $t$, the context splits up naturally as $\Delta;\Gamma$, where $\Gamma$ consists of those hypotheses of mode $t$ for which $\alpha_{nk} = 1_t$.

% The hypotheses in $\Delta$ can be of either mode, as can those in a judgment with conclusion of mode $v$.
% I'd like to say that in these cases we can go back and forth between the two kinds of hypotheses easily, but that seems to require Frobenius-ified versions of FL and UL.


\end{document}