\chapter{First-order logic}
\label{chap:fol}

\section{Predicate logic}
\label{sec:fol}

In \cref{sec:logic} we saw that the posetal reduction of a simple type theory can be regarded as a deductive system for logic (intuitionistic, linear, relevant, classical, etc.\ depending on the type theory).
However, these logics are only \emph{propositional}, lacking variables and the ability to quantify over them with statements such as ``for all $x$'' or ``there exists an $x$ such that''.
Similarly, in \cref{sec:fp-theories} we saw that simple type theory is adequate to express finite-product theories such as groups and rings, but not more complicated theories such as categories or fields.
The solution to both of these problems is the same: we combine \emph{two} type theories, one representing the objects (like a finite-product theory) and one representing the logic in which we speak about those objects.

The types in the second type theory, which we will henceforth call \textbf{propositions} instead of types to avoid confusion, will be \emph{dependent} on the types in the first type theory (which we sometimes call the \emph{base type theory}).
This means that terms belonging to types can appear in propositions.
More formally, it means that unlike the judgment $\types A \type$ for types (in the base type theory), the judgment for propositions \emph{has a context of types}, so we write it $\Gamma\types \ph\prop$.
We will have rules such as
\[ \inferrule*{\Gamma \types M:A \\ \Gamma\types N:A}{\Gamma\types (M =_A N)\prop} \]
allowing the logic (the type theory of propositions) to ``talk about'' equality of terms (morphisms between types).
Finally, since propositions depend on a context of types, their morphism judgment (which we also call \textbf{entailment}) must also depend on such a context.
Thus it has \emph{two} contexts, one of types and one of propositions, which we separate with a vertical bar: $\Gamma \cb \Theta \types \ph$.

In this section, we will describe and study type theories of this sort, with one simple type theory dependent on another simple type theory.
Unlike the type theories considered in \cref{chap:simple}, which were directly motivated by a corresponding categorical structure, in the present case it seems more natural to describe the type theory first and then define an appropriate categorical structure in order to match it.
(This is not to say that there are not lots of naturally occurring examples of this categorical structure; there are!
It's just that without the type theory in mind, we might not be led to define and study that exact class of categorical structures.)
Thus, we postpone consideration of their categorical semantics to \cref{sec:hyperdoctrines,sec:subobjects}.

We will also make several simplifying assumptions in this section.
Firstly, the base type theory will always be a bare theory of cartesian multicategories under some multigraph, with no type operations and no axioms.
The lack of axioms is not much of a problem, since once we have equality propositions we can use those instead.
The lack of type operations is a temporary simplification, but identifies our current subject as \emph{first-order} logic; in \cref{chap:hol} on ``higher-order logic'' we will reintroduce type operations.
The \emph{cartesianness} of the base type theory is also a simplifying assumption, but one that we will not (in this book) ever generalize away from.
People have attempted to define first-order logics over non-cartesian base theories, but in general the results are more complicated and less intuitive, and there are fewer interesting categorical examples.

Secondly, in this section the logic will be posetal, so that we care only about the existence of derivations rather than their values, and hence we will not introduce terms belonging to propositions.
We will generalize away from this assumption in \cref{sec:indexed-moncat}.


\subsection{Structural rules and simple rules}
\label{sec:fol-struc}

With all that out of the way, we move on to actually describing the rules.
As mentioned above, the base type theory is that for cartesian multicategories under a multigraph \cG:
\begin{mathpar}
  \inferrule{\types A\type \\ (x:A)\in \Gamma}{\Gamma\types x:A}\;\idfunc
  \and
  \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma\types M_1:A_1 \\ \cdots \\ \Gamma \types M_n:A_n}{\Gamma\types f(M_1,\dots,M_n):B}\;f
\end{mathpar}
As usual, cut/substitution is admissible for this theory.
For the propositions, we have two kinds of judgment:
\begin{mathpar}
  \Gamma\types \ph\prop \and
  \Gamma\cb\Theta\types \ph
\end{mathpar}
where $\Theta$ is a context (i.e.\ a list) of propositions.
Here the proposition $\ph$ should be regarded as a sort of ``term'' for the proposition judgment, that can be shown to uniquely determine a derivation of $\Gamma\types \ph\prop$.

Before discussing the rules for these judgments, however, we have to decide what to do about the structural rules such as cut.
As with propositional logic, we can formulate first-order logic in either a natural deduction or a sequent calculus style to make cut admissible.
However, I feel that both choices require formulating at least one of the rules for quantifiers and equality in a less-than-maximally-intuitive way.
Of course, intuitions differ from person to person.
But it is also a more objective fact that the most \emph{categorically natural} versions of the rules, as we will see in \cref{sec:hyperdoctrines}, also do not exactly match either the sequent calculus or the natural deduction versions.
There are also new structural rules, namely substitution of terms into propositions and entailments, that we would eventually like to be admissible as well.

For these reasons we take the following approach.
In this section we state all the structural rules, including both those that will stay primitive and those that will eventually be admissible.
Then in \crefrange{sec:forall}{sec:equality} we discuss the rules for the quantifiers and equality, mentioning all the ways that each rule can be formulated and showing that they are equivalent in the presence of all the structural rules.
Finally, in \cref{sec:fol-natded} we show that the natural deduction rules do make an appropriate selection of the structural rules admissible.
%Finally, in \cref{sec:fol-seqcalc,sec:fol-natded} we show that with a consistent choice of either the sequent calculus rules or the natural deduction rules we can make an appropriate selection of the structural rules admissible.

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule*[right=exchange]{\Gamma\cb\Theta,\ph,\psi,\Delta\types \chi}{\Gamma\cb\Theta,\psi,\ph,\Delta\types \chi}\and
    \inferrule*[right=weakening (maybe)]{\Gamma\cb \Theta,\Delta\types \chi}{\Gamma\cb\Theta,\ph,\Delta\types \chi}\and
    \inferrule*[right=contraction (maybe)]{\Gamma\cb\Theta,\ph,\ph,\Delta\types \chi}{\Gamma\cb\Theta,\ph,\Delta\types \chi}\and
    \inferrule*{ }{\Gamma\cb \ph\types\ph}\and
    \inferrule*{\Gamma\cb\Theta \types \ph \\ \Gamma\cb \Psi,\ph\types \psi}{\Gamma\cb \Psi,\Theta\types \psi}\and
    \inferrule*{\Gamma\types M:A \\ \Gamma,x:A\types \ph\prop}{\Gamma \types \ph[M/x] \prop}\and
    \inferrule*{\Gamma\types M:A \\ \Gamma,x:A\cb\Theta\types \ph}{\Gamma\cb\Theta[M/x] \types \ph[M/x]}\and
  \end{mathpar}
  \caption{Structural rules for first-order logic}
  \label{fig:fol-struc}
\end{figure}

The complete list of structural rules is shown in \cref{fig:fol-struc}.
As in \cref{sec:logic}, we always have exchange for propositions, but we allow ourselves the freedom to take or omit weakening and contraction, corresponding to a choice of a faithful cartesian club \fS (as in \cref{sec:cartmulti}).
Depending on which we choose, we speak of \textbf{intuitionistic first-order logic} (all the structural rules), \textbf{intuitionistic first-order linear logic} (exchange only), etc.

Then there are the identity and cut rule for propositions; the latter is just the cut rule from \cref{sec:monoidal-lattices} with an extra type context $\Gamma$.
There are also two new structural rules arising from the dependency of propositions on types: substitution of terms into propositions and into entailments.

Of all these structural rules, there is one that it is most important (for the purpose of categorical semantics) to make admissible: substitution of terms into propositions.
This is for the same reason that we want substitution into terms to be admissible.
Namely, we certainly want to be \emph{able} to make such substitutions, but if we asserted them as primitive then (to maintain the unique correspondence between names for propositions $\ph$ and the derivations of $\Gamma\types \ph\prop$) we would have to introduce ``$\ph[M/x]$'' as basic syntax, rather than an operation on syntax.

For instance, we want to be able to substitute $M$ for $x$ and $N$ for $y$ into $x=y$, and we want to be able to actually \emph{do} that substitution on the syntax to get $M=N$, rather than having to write $(x=y)[M/x,N/y]$ everywhere.
Another possibility would be to break the ``propositions are derivations'' correspondence and allow one proposition to have multiple derivations, but that has the same problems as breaking the ``terms are derivations'' correspondence in simple type theory; we do care about \emph{which} proposition we are talking about.

Fortunately, it is just as easy to ensure that substitution into propositions is admissible as it is to ensure that cut is admissible in a natural deduction.
We just make sure to ``build enough substitutions'' into the rules for the proposition judgment, so that their conclusions always have a fully general context.
Thus, we will always do this in our rules for the proposition judgment.

The other structural rules are all for entailment, and since at the moment we are interested in semantics where entailment corresponds to inequality in a poset, we only care about \emph{whether or not} an entailment is derivable rather than what all its derivations are.
Thus, it makes little difference (for the purpose of categorical semantics) whether these rules are primitive or admissible.
(However, there are still other technical advantages to admissibility.)
% some of which we will see later.

Now we move on to the logical rules for the proposition and entailment judgments.
To start with, there will be the usual rules for propositional logic from \cref{sec:logic}.
We import these rules into our present theory by assigning all of them an arbitrary context of types in the base theory that remains unchanged between the premises and the conclusion.
For instance, the rules for $\join$ are
\begin{mathpar}
  \inferrule{\Gamma\cb\Theta\types A}{\Gamma\cb\Theta\types A\join B}\;\joinI1
  \and
  \inferrule{\Gamma\cb\Theta\types B}{\Gamma\cb\Theta\types A\join B}\;\joinI2
  \and
  % \inferrule{
  %   \Gamma\cb\Theta,A \types C \\ \Gamma\cb\Theta,B\types C
  % }{\Gamma\cb\Theta,A\join B \types C}\;\joinL
  \inferrule{
    \Gamma\cb\Psi\types A\join B \\ \Gamma\cb\Theta,A \types C \\ \Gamma\cb\Theta,B\types C
  }{\Gamma\cb\Theta,\Psi \types C}\;\joinE
\end{mathpar}
and likewise we have rules for $\bot,\meet,\top,\tensor,\one$, and $\hom$.
%\footnote{Since cut is primitive, we could simplify the rules $\joinI1$ and $\joinI2$ to $\Gamma\cb A\types A\join B$ and $\Gamma\cb B\types A\join B$, or write $\joinE$ as a sequent-calculus-style left rule; but we will stick with the more familiar natural deduction versions.}
Of course, in the cartesian case we can dispense with $\tensor$ and $\one$ (since they coincide with $\meet$ and $\top$), and write $\hom$ instead as $\To$ or $\to$.
The modularity of type theory means we can also mix and match, choosing the rules corresponding to some of these connectives but not others; in \cref{sec:subobjects} we will see that some groups of connectives are particularly natural from a categorical perspective.

The interesting new things happen with the \emph{new} operations on propositions that \emph{do} change the type context.
We will consider three such operations, which are particularly natural both categorically and logically.
The first two are the \emph{quantifiers} ``for all'' (the ``universal quantifier'') and ``there exists'' (the ``existential quantifier'').
The rules introducing these two propositions both look the same:
\begin{mathpar}
  \inferrule{\Gamma,x:A\types \ph\prop}{\Gamma\types (\forall x:A.\ph) \prop}\and
  \inferrule{\Gamma,x:A\types \ph\prop}{\Gamma\types (\exists x:A.\ph) \prop}\and
\end{mathpar}
(Note that in both cases the variable $x$ is \emph{bound} in the resulting proposition, just as it is in $\lambda x.M$.
If there is no danger of confusion, we may abbreviate these to $\all x.\ph$ and $\exis x.\ph$, but in general the type annotation is necessary to make type-checking possible.)
But the rules governing entailments involving them, of course, are different.

Recall that in natural deduction each type operation has either \emph{introduction} and \emph{elimination} rules, while in sequent calculus these are reformulated as \emph{right} and \emph{left} rules.
In the past we have motivated these rules by appeal to universal properties in a categorical structure, with one group of rules giving the basic data and the other giving their universal factorization property.
The rules for $\exis$ and $\all$ do correspond to universal properties, but since we have postponed the semantics of first-order logic to \cref{sec:hyperdoctrines} we will attempt to instead motivate their rules from an intuitive understanding of logic.

\subsection{The universal quantifier}
\label{sec:forall}

Informally, how do we prove that $\forall x:A.\ph$?
Arguably the most basic way to do it is to assume given an arbitrary $x:A$ and prove that $\ph$ is true (here $\ph$ is a statement involving $x$, hence involving our arbitrary assumed $x:A$).
This suggests the following introduction (or right) rule:
\begin{mathpar}
  \inferrule{\Gamma,x:A\cb \Theta\types \ph}{\Gamma\cb\Theta\types \forall x:A.\ph}\;\forallI
\end{mathpar}
Note that since $\Theta$ appears in the conclusion, where $x$ is no longer in the type context, $\Theta$ cannot depend on $x$, even though syntactically the premise would allow that.

Similarly, what good does it do to know that $\forall x:A.\ph$?
The most basic thing it tells us is that if we have any particular element $M$ of $A$, then $\ph$ is true about $M$, i.e.\ with $M$ replacing $x$.
The simplest way to formulate this is
\begin{mathpar}
  \inferrule{\Gamma\types M:A}{\Gamma\cb (\forall x:A.\ph) \types \ph[M/x]}\;\forallS
\end{mathpar}
But there are many other ways to say the same thing, including a sequent-calculus-style left rule, a natural-deduction-style elimination rule, and the opposite of the introduction rule:
\begin{mathpar}
  \inferrule{\Gamma\types M:A \\ \Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma\cb\Theta\types \ph[M/x]}\;\forallE\and
  \inferrule{\Gamma\types M:A \\ \Gamma\cb \Theta, \ph[M/x] \types \psi}{\Gamma\cb \Theta, (\forall x:A.\ph) \types \psi}\;\forallL\and
  \inferrule{\Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma,x:A\cb \Theta\types \ph}\;\forallI^{-1}
\end{mathpar}
All of these rules are inter-derivable in the presence of cut and substitution.
For instance, we can derive $\forallE$ from $\forallI^{-1}$ using substitution:
\begin{mathpar}
  \inferrule*[right=sub]{\Gamma\types M:A \\
    \inferrule*[Right=$\forallI^{-1}$]{\Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma,x:A\cb \Theta\types \ph}
  }{\Gamma\cb\Theta\types \ph[M/x]}
\end{mathpar}
We can derive $\forallS$ as a special case of $\forallE$ using the identity rule:
\begin{mathpar}
  \inferrule*[right=$\forallE$]{\Gamma\types M:A\\
  \inferrule*{ }{\Gamma\cb (\forall x:A.\ph)\types \forall x:A.\ph}
  }{\Gamma\cb (\forall x:A.\ph) \types \ph[M/x]}
\end{mathpar}
We can derive $\forallL$ from $\forallS$ using cut:
\begin{mathpar}
  \inferrule*[right=cut]{
    \inferrule*[right=$\forallS$]{\Gamma\types M:A}{\Gamma\cb (\forall x:A.\ph) \types \ph[M/x]} \\
    \Gamma\cb \Theta, \ph[M/x] \types \psi}{\Gamma\cb \Theta, (\forall x:A.\ph) \types \psi}
\end{mathpar}
and finally $\forallI^{-1}$ from $\forallL$ using cut and weakening:
\begin{mathpar}
  \inferrule*[right=cut]{
    \inferrule*[right=weak]{\Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma,x:A\cb\Theta\types \forall x:A.\ph}\\
    \inferrule*[Right=$\forallL$]{
      \inferrule*{ }{\Gamma,x:A\types x:A} \\
      \inferrule*{ }{\Gamma,x:A\cb \ph \types \ph}}
    {\Gamma,x:A\cb (\forall x:A.\ph) \types \ph}}
  {\Gamma,x:A\cb \Theta\types \ph}
\end{mathpar}
In practice, therefore, we are free to use whichever rule we find most intuitive or convenient.
To make substitition and cut admissible in \cref{sec:fol-natded} we will use $\forallE$, while for categorical semantics in \cref{sec:hyperdoctrines} we will use $\forallI^{-1}$.

\begin{rmk}
  Note that many of these rules involve substitution into propositions.
  Thus, formally speaking we have to state all the rules for the proposition judgment $\Gamma\types \ph\prop$ first, \emph{then} prove that substitution into propositions is admissible (thereby defining the notation $\ph[M/x]$), and only after that can we state all the rules for the entailment judgment $\Gamma\cb\Theta\types\ph$.
  A similar situation obtained for the equality judgment $\equiv$ for simple and unary type theories, which often involved substitution into terms (e.g.\ $(\lambda x.M)N \equiv M[N/x]$), so that we had to prove the admissibility of the latter before stating the rules for $\equiv$ (and likewise, when proving the initiality theorems, we had to show that our functor-in-progress took substitution to composition before defining it on equalities).
  However, in practice we actually state all the rules at once, with the implicit understanding that afterwards we will define substitution so that the rules involving it make sense.

  We do have to be careful, when taking such a shortcut, to notice whether we are introducing any ``cyclic dependencies''.
  For instance, if there are any rules for the term or proposition judgments whose premises involve the entailment judgment, it is no longer possible to complete the definition of the former, \emph{then} define substitution for them, and \emph{then} give the definition of the latter: we would have to give the definition all at once, including (somehow) defining substitution at the same time.
  It is possible to do this, but it is much more difficult and leads us into the realm of dependent type theory; see \cref{chap:dtt}.

  In this chapter and \cref{chap:hol} none of our rules will introduce such cyclic dependencies.
  We mention the possibility only as a warning to the reader, because it is easy (especially when adding rules to a type theory one by one) to fail to notice a cyclic dependency when it appears.
  %See also \cref{rmk:subset-quotient}.
\end{rmk}


\subsection{The existential quantifier}
\label{sec:exists}

% [TODO: Remind the extra context as needed for modeling natural reasoning here?]

The most basic way to prove $\exists x:A.\ph$ is to exhibit a particular element $M$ of $A$ and prove that it has the property $\ph$ (that is, $\ph$ with $M$ replacing $x$ is true).
This is of course a ``constructive'' proof.
In classical mathematics one can also give ``nonconstructive'' existence proofs, but these arise by use of the law of excluded middle or its equivalent law of double negation.
The \emph{basic} way to prove existence, which uses no other logical laws than the meaning of ``existence'', is to supply a witness.
This leads to the following introduction (or right) rule for $\exis$:
\begin{mathpar}
  \inferrule{\Gamma\types M:A \\ \Gamma\cb\Theta\types \ph[M/x]}{\Gamma\cb\Theta\types \exists x:A.\ph}\;\existsI
\end{mathpar}

On the other hand, what good does it do to know that $\exists x:A.\ph$?
It means we are free to assume that we have some element of $A$ satisfying $\ph$ (but about which we assume nothing else).
This is most simply expressed by a left rule:
\begin{mathpar}
  \inferrule{\Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}\;\existsL\and
\end{mathpar}
This is perhaps the least intuitive of the quantifier rules: it says that if we can prove some other statement $\psi$ under the assumption of some arbitrary $x:A$ that satisfies $\ph$, then we can also conclude $\psi$ under the assumption of $\exists x:A.\ph$.
(Note the similarity in structure between $\existsL$ and $\tensorL$; this suggests the eventual universal property we will find corresponding to $\exis$.)

By building in a cut, we can re-express $\existsL$ as an elimination rule instead:
\begin{mathpar}
  \inferrule{\Gamma\cb\Psi\types \exists x:A.\ph \\ \Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta,\Psi\types \psi}\;\existsE\and
\end{mathpar}
Of course $\existsE$ follows from $\existsL$ plus cut, while we can obtain $\existsL$ from $\existsE$ by taking $\Psi$ to be $(\exists x:A.\ph)$.

Technically, we should actually add some additional premises to $\existsE$ and $\existsL$ to ensure that $\psi$ and $\Theta$ are defined in context $\Gamma$ rather than $\Gamma,x:A$, since otherwise the premises would permit the latter.
Otherwise we would not want to let ourselves write $\Gamma\cb\Theta\types \psi$ (with $x$ not appearing in $\Gamma$, as implied by our conventions and the fact that in a premise we wrote $\Gamma,x:A$).
Thus we ought to write them as
\begin{mathpar}
  \inferrule{\Gamma \types \psi\prop \\
    \Gamma \types \Theta \ctx \\
    \Gamma,x:A\cb\Theta,\ph\types \psi
  }{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}\;\existsL\and
  \inferrule{\Gamma \types \psi\prop \\
    \Gamma \types \Theta \ctx \\
    \Gamma\cb\Psi\types \exists x:A.\ph \\
    \Gamma,x:A\cb\Theta,\ph\types \psi
}{\Gamma\cb\Theta,\Psi\types \psi}\;\existsE\and
\end{mathpar}
where $\Gamma \types \Theta \ctx$ is an abbreviation for
\[ \Gamma \types B_1\prop \quad\cdots\quad \Gamma\types B_n \prop\]
if $\Theta =(B_1,\dots, B_n)$.
However, we often neglect to write such conditions explicitly.

Finally, now that we have $\existsE/\existsL$, we note that $\existsI$ can also be reformulated in a couple of other ways:
\begin{mathpar}
  \inferrule{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}{\Gamma,x:A\cb\Theta,\ph\types \psi}\;\existsL^{-1}\and
  \inferrule{ }{\Gamma,x:A\cb\ph\types \exists x:A.\ph}\;\existsS
\end{mathpar}
These are both inter-derivable with $\existsI$ in the presence of cut and substitution.
For instance, we can deduce $\existsS$ as a special case of $\existsI$:
\begin{mathpar}
  \inferrule*[right=$\existsI$]{\inferrule*{ }{\Gamma,x:A\types x:A} \\
    \inferrule*{ }{\Gamma,x:A\cb\ph\types \ph}}
  {\Gamma,x:A\cb \ph\types \exists x:A.\ph}
\end{mathpar}
We can get $\existsL^{-1}$ from $\existsS$ and cut:
\begin{mathpar}
  \inferrule*[right=cut]{
    \inferrule*[right=$\existsS$]{ }{\Gamma,x:A\cb\ph\types \exists x:A.\ph}\\
    \inferrule*[Right=weak]{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}{\Gamma,x:A\cb\Theta,(\exists x:A.\ph)\types \psi}
  }{\Gamma,x:A\cb\Theta,\ph\types \psi}
\end{mathpar}
And we can get $\existsI$ by substituting and cutting in $\existsL^{-1}$:
\begin{mathpar}
  \inferrule*[right=cut]{
    \Gamma\cb\Theta\types \ph[M/x]\\
    \inferrule*[Right=sub]{\Gamma\types M:A \\
      \inferrule*[Right=$\existsL^{-1}$]{\Gamma\cb (\exists x:A.\ph)\types \exists x:A.\ph}{\Gamma,x:A\cb\ph\types \exists x:A.\ph
      }}{\Gamma\cb \ph[M/x] \types \exists x:A.\ph}
  }{\Gamma\cb\Theta\types \exists x:A.\ph}
\end{mathpar}
Thus, we are free to use whichever of these rules is most convenient.
To make substitition and cut admissible in \cref{sec:fol-natded} we will use $\existsE$ and $\existsI$, while for categorical semantics in \cref{sec:hyperdoctrines} we will use $\existsL$ and $\existsL^{-1}$.


\subsection{Equality}
\label{sec:equality}

The third and last new operation on propositions is perhaps the subtlest of all: the \emph{equality proposition}.
Its formation rule is unsurprising: it says that for any two terms of the same type, we can consider the proposition that they are equal.
\begin{mathpar}
  \inferrule{\Gamma\types M:A \\ \Gamma\types N:A}{\Gamma\types (M =_A N)\prop}
\end{mathpar}
(The subscript annotation $A$ in $M=_A N$ is needed for type-checking; but as usual, we will often omit it.)
But how are we to describe its behavior?
The most classical approach to equality is to assert that it is reflexive, symmetric, transitive, and ``substitutive'' (i.e.\ if $\ph[M/x]$ and $M=N$, then also $\ph[N/x]$).
This is very much like how we described the equality \emph{judgment} $M\equiv N$ in \cref{chap:unary,chap:simple}.
It works here too, but it doesn't fit the general introduction/elimination pattern of natural deduction, and therefore its categorical semantics are not as obvious.

It is one of the great insights of Lawvere~\cite{lawvere:comprehension} (presaged by Leibniz, and approximately contemporaneous with a similar observation by Martin-L\"of) that the rules of reflexivity, symmetry, transitivity, and substitutivity are equivalent to the following pair of rules:
\begin{mathpar}
  \inferrule{ }{\Gamma,x:A\cb \ec\types (x =_A x)}\;\eqR\and
  \inferrule{\Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]}{\Gamma,x:A,y:A\cb\Theta,(x =_A y)\types \ph}\;\eqL
  % \inferrule*{\Gamma\types M:A \\ \Gamma\types N:A \\\\ \Gamma,x:A,y:A\types \ph\prop \\ \Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]}{\Gamma\cb\Theta[M/x,N/y],(M=_A N)\types \ph[M/x,N/y]}
\end{mathpar}
The first, right/introduction, rule is simply reflexivity.
When combined with a substitution (to make substitution into entailment admissible) it becomes
\begin{equation}\label{eq:refl-withsub}
  \inferrule{\Gamma\types M:A}{\Gamma\cb \ec\types (M=_A M)}
\end{equation}
and if we have weakening, we can more generally derive $\Gamma\cb \Theta\types (M=_A M)$ for any proposition context $\Theta$.

The left rule is the tricky one to understand.
Intuitively, it says that if we have a statement about $x$ and $y$, and that statement becomes true when we substitute $x$ for $y$, then that statement is true under the hypothesis that $x=y$.
More generally, we can replace the truth of a statement with the truth of an entailment $\Theta\types \ph$, where we also substitute $x$ for $y$ in $\Theta$ in the premise.
In other words, \emph{if we have a hypothesis that $x=y$, then we may as well write $x$ instead of $y$ everywhere that it appears}.

To help motivate this rule further, let us derive symmetry and transitivity from it.
Here is symmetry:
\begin{mathpar}
  \inferrule*{x:A,y:A \types (y=_A x) \prop \\ \inferrule*{ }{x:A \cb \ec \types (x=_A x)}}{x:A,y:A \cb (x=_A y) \types (y=_A x)}
\end{mathpar}
We use the left rule once, with $\ph$ being $y=_A x$, so that $\ph[x/y]$ is $x=_A x$, which we can prove by reflexivity.

And here is transitivity:
\begin{mathpar}
  \inferrule*{
    x:A,y:A,z:A \types (x=_A z) \prop \\
    \inferrule*{ }{x:A,y:A \cb (x=_A y) \types (x=_A y)}
  }{x:A,y:A,z:A \cb (x=_A y),(y=_A z) \types (x=_A z)}
\end{mathpar}
We again use the left rule once on the hypothesis $y=_A z$, with $\ph$ being $x=_A z$, so that $\ph[y/z]$ is $x=_A y$, which we can prove by the identity rule from the other hypothesis.
Note that both symmetry and transitivity are \emph{derivable rules} in the sense of \cref{rmk:admissible-derivable-1}.

As with so many things, the only way to really understand this rule is to practice it.
We recommend the reader try their hand at \cref{ex:equality}.

There are a few more technical things to be said about $\eqL$.
Firstly, like $\existsL$, it should technically have additional premises making clear what $\Theta$ and $\ph$ are:
\begin{mathpar}
  \inferrule{
    \Gamma,x:A,y:A \types \ph\prop\\
    \Gamma,x:A,y:A \types \Theta\ctx\\
    \Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]
  }{\Gamma,x:A,y:A\cb\Theta,(x =_A y)\types \ph}
\end{mathpar}
Secondly, to make substitution into entailments admissible, it needs substitutions for $M$ and $N$ built in:
\begin{equation}\label{eq:J-withsub}
  \inferrule{
    \Gamma,x:A,y:A \types \ph\prop\\
    \Gamma,x:A,y:A \types \Theta\ctx\\\\
    \Gamma\types M:A\\
    \Gamma\types N:A\\
    \Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]
  }{\Gamma\cb\Theta[M/x,N/y],(M =_A N)\types \ph[M/x,N/y]}
\end{equation}
Thirdly, to make cut for propositions admissible, it needs another cut built in as well; see \cref{fig:fol-natded}.


\subsection{First-order theories}
\label{sec:first-order-theories}

The last thing we need is some ``generator'' rules that would allow us to speak of a ``first-order theory''.
In addition to our multigraph \cG giving the base types and terms, we would like to also have a set \cP of ``base propositions'' (usually called \textbf{atomic propositions}).
Each of these should have an assigned \emph{type context}, i.e.\ a list of objects of \cG; we write $\cP(A_1,\dots,A_n)$ for the set of atomic propositions with context $A_1,\dots,A_n$.
Then we will have a generator rule for propositions, with substitutions built in just like the generator rule for terms:
\[ \inferrule{P\in \cP(A_1,\dots,A_n) \\ \Gamma\types M_1:A_1 \\ \cdots\\ \Gamma\types M_n:A_n}{\Gamma \types P(M_1,\dots,M_n) \prop} \]

\begin{rmk}
  Note that while we write $\ph$ for a \emph{generic} proposition that might contain a variable $x$, and $\ph[M/x]$ for the result of substituting $M$ for that variable $x$, if $P$ is an \emph{atomic} proposition we write $P(x)$ and $P(M)$ for its instantiations at a variable $x$ or a more general term $M$.
  As always, substitution $\ph[M/x]$ is an \emph{operation} on propositions; while the application $P(M)$ is, like the application of a function symbol $f(M)$, a \emph{primitive} part of syntax.
  The relationship between them is that $(P(x))[M/x]$ is, by definition, $P(M)$ (see \cref{thm:fol-subprop-adm}).
\end{rmk}

\begin{rmk}
  There is a substantial tradition of terminology according to which the phrase \emph{atomic proposition} includes not just these ``generating'' propositions, but also \emph{equality} propositions $(M=_A N)$.
  This is entirely understandable historically, since when equality is presented using laws such as reflexivity, symmetry, transitivity, and substitution it appears ``axiomatic'' rather than governed by principled rules like those of the connectives and quantifiers.
  However, from a modern (i.e.\ post-Lawvere~\cite{lawvere:comprehension}) perspective, we can see that the rules $\eqR$ and $\eqL$ have the same shape as those of the other connectives and quantifiers, and in \cref{sec:hyperdoctrines} we will see that they similarly express a categorical universal property.
  Thus, it makes much more sense to call the equality rules \emph{logical}, like those of the connectives and quantifiers, and restrict the adjective \emph{atomic} to the generating propositions.
\end{rmk}

Finally, we should have some generating entailments, i.e.\ \emph{axioms}.
Each of these should have an assigned type context $A_1,\dots,A_n$, an assigned proposition context $\Theta$, and an assigned consequent $\ph$.
Here $\ph$ and the elements of $\Theta$ should be propositions in context $x_1:A_1,\dots,x_n:A_n$ --- not just atomic propositions, but arbitrary ones derivable from the atomic ones and the rules for making new propositions.
If we write $\cA(A_1,\dots,A_n;\Theta;\ph)$ for the assertion that there is such an axiom, then simplest form of the generator rule introducing axioms will be
\[ \inferrule{\cA(A_1,\dots,A_n;\Theta;\ph)}{x_1:A_1,\dots,x_n:A_n \cb \Theta \types \ph} \]
To make substitution into entailments admissible, we should build one in:
\[ \inferrule{\cA(A_1,\dots,A_n;\Theta;\ph) \\ \Gamma\types M_1:A_1 \\ \cdots\\ \Gamma\types M_n:A_n}{\Gamma \cb \Theta[\vec M/\vec x]\types \ph[\vec M/\vec x]} \]
And to make cut admissible we should also build in a cut; see \cref{fig:fol-natded}.

With this rule added to the other rules for entailment, we complete the definition of \textbf{intuitionistic first-order \fS-logic}.
If we include both weakening and contraction, we speak simply of \textbf{intuitionistic first-order logic}, while other values of \fS have appropriate names like \textbf{intuitionistic first-order linear logic} (no weakening or contraction) and so on.
A \textbf{first-order theory} in any such logic consists of all the generating data:
\begin{enumerate}
\item A set of \emph{objects} (also called \emph{types} or \emph{sorts});
\item A set of \emph{morphisms} (also called \emph{function symbols}), each with a list of objects as its domain and a single object as its codomain;
\item A set of \emph{atomic propositions} (also called \emph{predicates} or \emph{relation symbols}), each with a list of objects as its domain or arity; and
\item A set of \emph{axioms}, each consisting of a type context, a proposition context, and a consequent.
\end{enumerate}

The qualifier ``intuitionistic'' is because, like in \cref{sec:logic}, we cannot prove the law of excluded middle $\ph\join\neg\ph$ (where $\neg\ph$ means $\ph\hom\bot$), or its equivalent the law of double negation $\neg\neg\ph\hom\ph$.
In \cref{sec:logic} we motivated this by noting that leaving it out just means our ``logic'' has models in all Heyting algebras rather than just Boolean algebras.
We will be able to say something similar, and hopefully even more convincing, about first-order logic in \cref{sec:subobjects}.

A few important subsystems of intuitionistic first-order logic that will reappear later are:
\begin{itemize}
\item \emph{Coherent} logic: includes $\meet,\top,\join,\bot,\exis,=$ but not $\To$ or $\all$ (hence also not $\neg$).
\item \emph{Regular} logic: includes $\meet,\top,\exis,=$ but not $\join,\bot,\To,\neg,\all$.
\item \emph{Horn} logic: includes $\meet,\top,=$ but not $\join,\bot,\To,\neg,\all,\exis$.
% \item \emph{Left-exact} or \emph{finite-limit} logic: includes $\meet,\top,=$ but not $\join,\bot,\To,\all,\exis$.  [TODO: Need a restricted form of $\exis$, which ties a partial knot between propositions and entailment, hence including substitution too.]
\item Another important logic is \emph{geometric} logic, which is like coherent logic but also includes the ``infinitary disjunction'' from \cref{ex:frames}.
\item In \cref{sec:lex-theories} we will study a somewhat more complicated logic to define called \emph{finite-limit} or \emph{lex logic}.
\end{itemize}


\subsection{Natural deduction}
\label{sec:fol-natded}

At last we are ready to consider admissibility of substitution and cut.
To be precise, we work with the \textbf{natural deduction for first-order intuitionistic \fS-logic} consisting of:
\begin{enumerate}
\item The rules for forming terms and propositions; % summarized in \cref{fig:fol-common};
\item The exchange and possibly (depending on \fS) weakening and contraction rules;
\item The identity rule $\Gamma \cb \ph\types\ph$ for all propositions $\ph$;
\item The natural deduction rules for intuitionistic \fS-logic from \cref{fig:natded-logic}, with an arbitrary type context $\Gamma$; and
\item The natural deduction rules for quantifiers, equality, and axioms summarized in \cref{fig:fol-natded}.
\end{enumerate}
Of course, the modularity of type theory means we can mix and match these rules, removing any number of type operations and their corresponding rules without altering the main theorems.
%(In particular, in the cartesian case we generally omit $\tensor$ and $\one$, since they are isomorphic to $\meet$ and $\top$.)

% \begin{figure}
%   \centering
%   \begin{mathpar}
%   \inferrule{\types A\type \\ (x:A)\in \Gamma}{\Gamma\types x:A}\and
%   \inferrule{f\in \cG(A_1,\dots,A_n;B) \\ \Gamma\types M_1:A_1 \\ \cdots \\ \Gamma \types M_n:A_n}{\Gamma\types f(M_1,\dots,M_n):B}\and
%   \inferrule{P\in \cP(A_1,\dots,A_n) \\ \Gamma\types M_1:A_1 \\ \cdots\\ \Gamma\types M_n:A_n}{\Gamma \types P(M_1,\dots,M_n) \prop}\and
%   \inferrule{\Gamma\types \ph\prop \\ \Gamma\types\psi\prop}{\Gamma\types (\ph\tensor\psi)\prop}\and
%   \inferrule{ }{\Gamma\types \one\prop}\and
%   \inferrule{\Gamma\types \ph\prop \\ \Gamma\types\psi\prop}{\Gamma\types (\ph\meet\psi)\prop}\and
%   \inferrule{ }{\Gamma\types \top\prop}\and
%   \inferrule{\Gamma\types \ph\prop \\ \Gamma\types\psi\prop}{\Gamma\types (\ph\join\psi)\prop}\and
%   \inferrule{ }{\Gamma\types \bot\prop}\and
%   \inferrule{\Gamma\types \ph\prop \\ \Gamma\types\psi\prop}{\Gamma\types (\ph\hom\psi)\prop}\and
%   \inferrule{\Gamma,x:A\types \ph\prop}{\Gamma\types (\forall x:A.\ph) \prop}\and
%   \inferrule{\Gamma,x:A\types \ph\prop}{\Gamma\types (\exists x:A.\ph) \prop}\and
%   \inferrule{\Gamma\types M:A \\ \Gamma\types N:A}{\Gamma\types (M =_A N)\prop}
%   \end{mathpar}
%   \caption{Rules for terms and propositions}
%   \label{fig:fol-common}
% \end{figure}

\begin{figure}
  \centering
  \begin{mathpar}
    \inferrule{\Gamma,x:A\cb \Theta\types \ph}{\Gamma\cb\Theta\types \forall x:A.\ph}\;\forallI\and
    \inferrule{\Gamma\types M:A \\ \Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma\cb\Theta\types \ph[M/x]}\;\forallE\and
    \inferrule{\Gamma\types M:A \\ \Gamma\cb\Theta\types \ph[M/x]}{\Gamma\cb\Theta\types \exists x:A.\ph}\;\existsI\and
    \inferrule{\Gamma\cb\Psi\types \exists x:A.\ph \\ \Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta,\Psi\types \psi}\;\existsE\and
    \inferrule{\Gamma\types M:A}{\Gamma\cb \ec\types (M=_A M)}\;\eqI\and
    \inferrule{
      \Gamma\types M:A\\
      \Gamma\types N:A\\
      \Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]\\
      \Gamma\cb \Psi \types (M =_A N)\\
      \Gamma\cb \Phi\types \Theta[M/x,N/y]
    }{\Gamma\cb\Phi,\Psi\types \ph[M/x,N/y]}\;\eqE\and
    \inferrule{\cA(A_1,\dots,A_n;\Theta;\ph) \\
      \Gamma\types M_1:A_1 \\ \cdots\\ \Gamma\types M_n:A_n \\
      \Gamma \cb \Phi \types \Theta[\vec M/\vec x]
    }{\Gamma \cb \Phi \types \ph[\vec M/\vec x]}\;\textsc{axiom}
  \end{mathpar}
  \caption{Natural deduction rules for quantifiers, equality, and axioms}
  \label{fig:fol-natded}
\end{figure}

Note also that the rules $\eqE$ and \textsc{axiom} from \cref{fig:fol-natded} incorporate an additional cut on the left.
For this we have used a shortcut notation $\Gamma\cb \Phi\types \Theta$ where $\Theta$ is a proposition context, meaning that $\Gamma\cb \Phi\types \theta$ for each $\theta\in\Theta$.

We start with the admissibility of substitution into propositions.

\begin{thm}\label{thm:fol-subprop-adm}
  Substitution into propositions is admissible: given derivations of $\Gamma,x:A \types \ph\prop$ and $\Gamma\types M:A$, we can construct a derivation of $\Gamma \types \ph[M/x]\prop$.
\end{thm}
\begin{proof}
  As with substitution into terms, this is entirely straightforward because we have written all the rules for such judgments with an arbitrary type context.
  Some of the defining clauses are
  \begin{align*}
    (\ph\meet\psi)[M/x] &= \ph[M/x] \meet \psi[M/x]\\
    (\forall y:B.\ph)[M/x] &= \forall y:B.\ph[M/x]\\
    (N=_B P)[M/x] &= (N[M/x] =_B P[M/x])
  \end{align*}
  In the case of $\all$ (and also $\exis$), we have to ensure (by $\alpha$-equivalence if necessary) that $x$ and $y$ are distinct variables, and that $y$ does not occur in $M$.
  This is the same issue that arose in \cref{sec:multicat-moncat,sec:multicat-prod-coprod,sec:stlc} when substituting into terms with bound variables such as $\case$ and $\lambda$-abstractions.
  As always, this is only an issue when representing derivations by terms; the underlying operation on derivations has no notion of ``bound variable''.

  Note also that substitution into an equality \emph{proposition} is defined using substitution into the \emph{terms} appearing in it.
  But since terms never involve propositions, there is no cyclic dependency: we can first prove the admissibility of substitution into terms, and then use it to prove the admissibility of substitution into propositions.
\end{proof}

Just as substitution into terms is associative, substitution into propositions satisfies as ``functoriality'' property that can be proven in the same way:
\begin{equation}
  \ph[N/y][M/x] = \ph[M/x][N[M/x]/y]\label{eq:fol-subprop-funct}
\end{equation}

\begin{thm}\label{thm:fol-subent-adm}
%  If we avoid the rules $\forallI^{-1}$, $\existsL^{-1}$, and $\existsS$, and formulate the equality rules with substitutions as in~\eqref{eq:refl-withsub} and~\eqref{eq:J-withsub}, then
  Substitution into entailments is admissible: if we have derivations of $\Gamma,x:A \types\Theta\types \ph$ and $\Gamma\types M:A$, we can construct a derivation of $\Gamma \types \Theta[M/x] \types \ph[M/x]$.
\end{thm}
\begin{proof}
  Just like \cref{thm:fol-subprop-adm}, we substitute recursively into the derivation of $\Gamma,x:A \types\Theta\types \ph$.
  This works because all the entailment rules have a fully general type context in the conclusion, so the substitution can always be done inductively on their premises.
\end{proof}

\begin{thm}\label{thm:fol-natded-cutadm}
  Cut for propositions is admissible in the natural deduction for first-order intuitionistic \fS-logic: given derivations of $\Gamma\cb\Theta \types \ph$ and $\Gamma\cb \Psi,\ph\types \psi$, we can construct a derivation of $\Gamma\cb \Psi,\Theta\types \psi$.
\end{thm}
\begin{proof}
  As usual, we induct on the derivation of $\Gamma\cb \Psi,\ph\types \psi$.
  This works because all the rules for the natural deduction have a fully general proposition context in the conclusion as well.
\end{proof}

As in \cref{sec:heyting-algebras}, in the cartesian case we can make exchange, weakening, and contraction admissible as well, by reformulating the rules $\existsE$ and $\eqE$ to keep the same proposition context in the premises and the conclusion, and the identity rule to incorporate a weakening.
The reformulated rules are
\begin{mathpar}
  \inferrule{\Gamma\cb\Theta\types \exists x:A.\ph \\ \Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta\types \psi}\;\existsE'\and
  \inferrule{
    \Gamma\types M:A\\
    \Gamma\types N:A\\
    \Gamma,x:A\cb\Phi,\Theta[x/y]\types \ph[x/y]\\
    \Gamma\cb \Phi \types (M =_A N)\\
    \Gamma\cb \Phi\types \Theta[M/x,N/y]
  }{\Gamma\cb\Phi\types \ph[M/x,N/y]}\;\eqE'\and
\end{mathpar}
We leave the proof to the reader (\cref{ex:fol-natded-strucadm}).

Recall also from \cref{sec:natded-logic} that with such a reformulation, the natural deduction of intuitionistic propositional logic can be formulated without explicit contexts, instead ``discharging'' temporary assumptions by crossing them out.
The same is true for intuitionistic first-order logic with $\all$ and $\exis$, if we also allow ``assumptions of variables'' (i.e.\ additions to the type context, in addition to the proposition context, as we move up the derivation tree) that can be discharged by the quantifier rules.
Usually we do not bother to include the derivations of term judgments in this style; we just write down the terms wherever they are needed.

For instance, here is a derivation in this style of the intuitionistic tautology $\ph\meet (\exists x:A.\psi) \To (\exists x:A. (\ph\meet\psi))$.
\[
\inferrule*[Right=$\ToI$]{
  \inferrule*[Right=$\existsE'$]{
    \inferrule*{\cancel{\ph\meet (\exists x:A.\psi)}}{\exists x:A.\psi}\\
    \inferrule*[Right=$\existsI$]{
      \cancel{x:A}\\
      \inferrule*[Right=$\meetI$]{
        \inferrule*{\cancel{\ph\meet (\exists x:A.\psi)}}{\ph} \\
        \cancel{\psi}
      }{\ph \meet \psi}
    }{\exists x:A. (\ph\meet\psi)}}{\exists x:A. (\ph\meet\psi)}
}{\ph\meet (\exists x:A.\psi) \To (\exists x:A. (\ph\meet\psi))}
\]
% (In a perhaps-misguided attempt at clarification, we have used a different variable for one of the quantifiers.)
% \[
% \inferrule*[right=$\alpha$-equiv]{
%   \inferrule*[Right=$\ToI$]{
%   \inferrule*[Right=$\existsE'$]{
%     \inferrule*{\cancel{\ph\meet (\exists x:A.\psi)}}{\exists x:A.\psi}\\
%     \inferrule*[Right=$\existsI$]{
%     \cancel{x:A}\\
%     \inferrule*[Right=$\meetI$]{
%       \inferrule*{\cancel{\ph\meet (\exists x:A.\psi)}}{\ph} \\
%       \inferrule*[Right=i.e.]{\cancel{\psi}}{\psi[y/x][x/y]}
%     }{\ph \meet \psi[y/x][x/y]}
%   }{\exists x:A. (\ph\meet\psi[y/x])}}{\exists y:A. (\ph\meet\psi[y/x])}
% }{\ph\meet (\exists x:A.\psi) \To (\exists y:A. (\ph\meet\psi[y/x]))}}
% {\ph\meet (\exists x:A.\psi) \To (\exists x:A. (\ph\meet\psi))}
% \]
The hypotheses $x:A$ and $\psi$ are discharged by the $\existsE'$, while the two occurences of the hypothesis ${\ph\meet (\exists x:A.\psi)}$ are discharged by the $\ToI$.
Without too much stretch, this can be regarded as a direct formalization of the following informal English proof:
\begin{quote}
  Suppose ${\ph\meet (\exists x:A.\psi)}$, that is $\ph$ and $\exists x:A.\psi$.
  By the latter, we may assume given an $x$ such that $\psi$.
  Now we have both $\ph$ and $\psi$, so $\ph\meet\psi$.
  Thus, $\exists x:A. (\ph\meet\psi)$, and so we have $\ph\meet (\exists x:A.\psi) \To (\exists x:A. (\ph\meet\psi))$.
\end{quote}

\begin{rmk}
  In particular, this (nontrivial!)\ interaction between $\meet$ and $\exis$ is, like the distributive law of $\meet/\tensor$ over $\join$ from \cref{ex:monpos-jslat} and \cref{sec:logic}, implied automatically by the structure of our contexts and how they interact with the rules for $\meet$ and $\exis$.
  There is sometimes a temptation to ``simplify'' logic by presenting it as a unary type theory, arguing that a context $\Theta = (\ph_1,\dots,\ph_n)$ can always be replaced by the conjunction $\ph_1\meet \dots \meet\ph_n$, and perhaps even replacing entailments $\ph\types \psi$ by implications $\ph\To\psi$.
  This is technically possible, but it forces one to assert laws like these ``by hand'', breaking principle~\eqref{princ:independence} and making for a less congenial theory.
  More importantly, as remarked in \cref{sec:natded-logic}, allowing arbitrarily many propositions in the context yields a formal theory that matches informal reasoning much better: as in the example above, informally we frequently apply inference rules in the presence of other unaffected hypotheses.

  Furthermore, for categorical semantics it is important to maintain the distinction between entialment and implication, since entailment corresponds to a morphism in a category, whereas implication corresponds to an internal-hom in a category.
  In particular, the former always exists, but the latter may not.
  Phrasing the rules for logical operations such as $\exis$ and $\join$ in a way that matches ordinary reasoning, \emph{and} doesn't refer to any other operations such as $\To$, ensures that ordinary informal (constructive) reasoning can be formalized and remain valid in any category as long as it uses only operations that exist in that category.
  This is important because we will see in \cref{sec:subobjects} that certain fairly natural conditions on categories allow them to model some, but not always all, of the logical operations.
\end{rmk}

The rule $\eqE'$ is a bit tricker to write in this style because of the arbitrary context $\Theta$ that has to be substituted into.
One approach is to use \cref{ex:eq-frob-from-hom}, which shows that as long as we also have implication we can get around this.
A more direct approach is to allow the proof of $\ph[x,y]$ to discharge an arbitrary number of hypotheses of the form $\theta[x/y]$, as long as we also supply corresponding proofs of $\theta[M/x,N/y]$ to the rule $\eqE'$.
For instance, with one $\theta$ formula the rule would look like this:
\[
\inferrule*{
  \inferrule*{\vdots}{M =_A N}\\
  \inferrule*{\vdots}{\theta[M/x,N/y]}\\
  \inferrule*{\mprset{fraction={\relax\relax\relax}}\inferrule*{\cancel{x:A} \\ \cancel{\theta[x/y]}}{\vdots}}{\ph[x/y]}
  }{\ph[M/x,N/y]}
\]


% \subsection{Sequent calculus}
% \label{sec:fol-seqcalc}

% The rules for \textbf{first-order intuitionistic \fS-sequent-calculus} consist of
% \begin{enumerate}
% \item The standard rules for types, terms, and propositions shown in \cref{fig:fol-common} (omitting $\tensor$ and $\one$ in the cartesian case);
% \item The exchange and possibly (depending on \fS) weakening and contraction rules;
% \item The identity rule $\Gamma \cb \ph\types\ph$ \emph{only when $\ph$ is an instance of an atomic proposition};
% \item The sequent calculus rules for intuitionistic \fS-logic from \cref{sec:seqcalc-logic}, with an arbitrary type context $\Gamma$; and
% \item The sequent calculus rules for quantifiers and equality summarized in \cref{fig:fol-seqcalc}.
% \end{enumerate}

% \begin{figure}
%   \centering
%   \begin{mathpar}
%     \inferrule{\Gamma,x:A\cb \Theta\types \ph}{\Gamma\cb\Theta\types \forall x:A.\ph}\;\forallR\and
%     \inferrule{\Gamma\types M:A \\ \Gamma\cb \Theta, \ph[M/x] \types \psi}{\Gamma\cb \Theta, (\forall x:A.\ph) \types \psi}\;\forallL\and
%     \inferrule{\Gamma\types M:A \\ \Gamma\cb\Theta\types \ph[M/x]}{\Gamma\cb\Theta\types \exists x:A.\ph}\;\existsR\and
%     \inferrule{\Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}\;\existsL\and
%     \inferrule{\Gamma\types M:A}{\Gamma\cb \ec\types (M=_A M)}\;\eqR\and
%     \inferrule{
%       \Gamma\types M:A\\
%       \Gamma\types N:A\\
%       \Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]
%     }{\Gamma\cb\Theta[M/x,N/y],(M =_A N)\types \ph[M/x,N/y]}\;\eqL\and
%      % TODO: What to do with this?
%   \end{mathpar}
%   \caption{Sequent calculus rules for quantifiers and equality}
%   \label{fig:fol-seqcalc}
% \end{figure}

% TODO: Has cut-admissibility for sequent calculus been done using Lawvere's equality rule?

% Need to build in cuts on both sides of axioms in general, as mentioned in \cref{sec:unary-theories}.


\subsection*{Exercises}

\begin{ex}\label{ex:eq-frob-from-hom}
  Assuming we have $\hom$, show that the rule $\eqR$ is derivable (recall \cref{rmk:admissible-derivable-1}) from the following simpler rule with no proposition context $\Theta$:
  \begin{mathpar}
    \inferrule{\Gamma\types M:A \\ \Gamma\types N:A \\\\ \Gamma,x:A,y:A\types \ph\prop \\ \Gamma\types\Theta\ctx \\ \Gamma,x:A\cb\Theta \types \ph[x/y]}{\Gamma\cb\Theta,(M=_A N)\types \ph[M/x,N/y]}
  \end{mathpar}
\end{ex}

\begin{ex}\label{ex:quantifier-laws}
  Three of the following four sequents are derivable in intuitionistic first-order logic (for any type $A$,  context $\Gamma$, and proposition $\Gamma,x:A\types\ph\prop$); derive them.
  \begin{align*}
    \Gamma \cb \exists x:A. \neg \ph &\types \neg\forall x:A. \ph\\
    \Gamma \cb \forall x:A. \neg \ph &\types \neg\exists x:A. \ph\\
    \Gamma \cb \neg\forall x:A. \ph &\types \exists x:A. \neg \ph\\
    \Gamma \cb \neg\exists x:A. \ph &\types \forall x:A. \neg \ph
  \end{align*}
\end{ex}

\begin{ex}\label{ex:equality}
  % CREDIT: Peter Lumsdaine
  In a first-order theory with
  three types $A$, $B$, $C$,
  two generating arrows $f : A \to B$ and $g : B \to A$,
  one atomic proposition $P$ with domain $(A,B)$, and
  no axioms,
  derive the following judgments:
  \begin{enumerate}
  \item $x_1: A, x_2 : A, y : B \cb \ph(x_1,y), (x_1 =_A x_2) \types \ph(x_2,y)$
  \item $x_1 : A, x_2 : A \cb (x_1 =_A x_2) \types f(x_1) =_B f(x_2)$
  \item $\ec \cb ( \forall x : A. g(f(x)) =_A x ) \types \forall x_1:A. \forall x_2 : A. \left((f(x_1) =_B f(x_2)) \to (x_1 =_A x_2) \right)$
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:fol-egs}
  Write down a first-order theory for each of the following structures.
  If you can, formulate them so that they fit inside the specified fragment.
  \begin{enumerate}
  \item Partially ordered sets (Horn)
  \item Totally ordered sets (coherent)
  \item Fields (coherent)
  \item Categories (regular)
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:fol-natded-strucadm}
  Prove that in intuitionistic first-order logic with $\existsE$ and $\eqE$ replaced by $\existsE'$ and $\eqE'$ as mentioned at the end of the section, the structural rules of exchange, weakening, and contraction for proposition contexts are admissible.
\end{ex}


\section{First-order hyperdoctrines}
\label{sec:hyperdoctrines}

Now we move on to the categorical semantics of first-order logic.
Continued adherence to principle~\eqref{princ:structural} suggests that the \emph{structural rules}, including for instance the substitution of terms into propositions and entailments, should correspond to basic operations in an appropriate categorical structure.
This would lead us to the following structure.

Let \fS be a faithful cartesian club, and recall from \cref{sec:cartmulti} the notion of \fS-multicategory and \fS-multiposet.
In contrast to \cref{chap:unary,chap:simple}, in this chapter we will assume for simplicity that our multiposets \emph{do} satisfy antisymmetry: if $x\le y$ and $y\le x$ then $x=y$.
Allowing distinct isomorphic objects, while morally correct, would lead us down a 2-categorical road that we prefer to postpone until \cref{sec:indexed-moncat}.

% TODO: A multicategory with a set-valued presheaf is the same as a polycategory with only 0,1-ary targets.

\begin{defn}
  Let \cS be a cartesian multicategory and \bC a category.
  A \textbf{\bC-valued presheaf on \cS} consists of
  \begin{enumerate}
  \item For each list $(A_1,\dots,A_n)$ of objects of \cS, an object $\cP(A_1,\dots,A_n)\in\bC$.
  \item For each list $(f_1,\dots,f_m)$ of morphisms of \cS, with $f_i:(A_{i1},\dots,A_{in_i})\to B_i$, a morphism in \bC:
    \[ (f_1,\dots,f_n)^* : \cP(B_1,\dots,B_m) \to \cP(A_{11},\dots,A_{mn_m}) \]
  \item These morphisms are associative and unital with respect to composition in \cS:
    \begin{align*}
      (f_{11},\dots,f_{mn_m})^* \circ (g_1,\dots,g_m)^* &=
      (g_1\circ (f_{11},\dots,f_{1n_1}), \dots, g_m \circ (f_{m1},\dots,f_{mn_m}))^*
      \\
      (\idfunc_{A_1},\dots,\idfunc_{A_n})^* &= \idfunc_{\cP(A_1,\dots,A_n)}
    \end{align*}
  \item For each $\sigma : \{1,\dots,m\} \to \{1,\dots,n\}$, a morphism in \bC:
    \[ \cP(A_{\sigma 1},\dots,A_{\sigma m}; B) \to \cP(A_1,\dots,A_n;B) \]
    satisfying analogues of the axioms in \cref{defn:fS-multicategory}.
  \end{enumerate}
\end{defn}

One way to understand the definition is that it is precisely the structure possessed by the contravariant representables: for any object $B$ in a cartesian multicategory \cS, there is a \bSet-valued presheaf $\cS(-;B)$.

Now the categorical structure corresponding to first-order logic should consist of a cartesian multicategory \bS and a presheaf \cP on \bS valued in the category of \fS-multiposets.
The objects and morphisms of \cS represent the types and terms, respectively; while
the objects of $\cP(A_1,\dots,A_n)$ represent the propositions in context $(A_1,\dots,A_n)$ and its morphisms/inequalities represent the entailments in that same context.
Composition in \cS represents substitution into terms, composition in each $\cP(A_1,\dots,A_n)$ represents the cut rule for propositions, and the functorial action of \cP represents substitution of terms into propositions and entailments.

However, in addition to being nonstandard, this structure is rather unnecessarily complicated.
It can be simplified greatly by the following observation, whose proof we leave to the reader (\cref{ex:pshf-multi-catprod}).

\begin{lem}\label{thm:pshf-multi-catprod}
  \bC-valued presheaves on a cartesian multicategory \cS are equivalent to ordinary \bC-valued presheaves on the category with finite products freely generated by \cS as in \cref{thm:free-catprod-cartmulti}.\qed
\end{lem}

Moreover, in practice we rarely care about semantics in cartesian multicategories that do not arise from categories with products.
Thus, we retreat slightly from the principled position of \cref{chap:simple}, and simplify our lives by taking the base \cS to be a category with products rather than a cartesian multicategory throughout.
This leads to the following definition.

\begin{defn}
  An \textbf{\cS-indexed \fS-multiposet} is a functor \cP from $\cS\op$ to the category of \fS-multiposets.
\end{defn}

Since we do not include product types in our base theory, this means that the free structure generated from a first-order logic will involve the \emph{category of contexts} introduced in \cref{sec:fp-theories}, and possess a universal property only up to equivalence.
For this reason we will often use letters like $\Gamma,\Delta$ for objects of \cS.
Thus, in this definition we have categorical counterparts of the type contexts (objects of \cS), terms (morphisms of \cS), substitution into terms (composition in \cS), propositions (objects of $\cP(\Gamma)$), entailments (morphisms of $\cP(\Gamma)$), cut for propositions (composition in $\cP(\Gamma)$), and substitution of terms into propositions and entailments (the functorial action of $\cP$).
In general for a morphism $f:\Gamma\to\Delta$ in \cS, we write $f^* : \cP(\Delta) \to \cP(\Gamma)$ for this latter action and call it a \textbf{reindexing} or \textbf{substitution} functor.

The propositional operations imported from \cref{sec:logic} are also easy to describe categorically.

\begin{defn}\label{defn:hyperdoctrine-heyting-fibers}
  Let \cP be an \cS-indexed \fS-multiposet.
  We say that \cP has \textbf{products}, \textbf{coproducts}, is \textbf{representable}, or is \textbf{closed}, if each \fS-multiposet $\cP(\Gamma)$ has the corresponding structure, and that structure is preserved by the reindexing functors $f^*$.
\end{defn}

We did not define formally in \cref{sec:multicats-catth} what it means for a functor to preserve all these properties of a multicategory, but we trust the reader can do it.
The requirement that $f^*$ preserve these properties is necessary because substitution in type theory does, by definition, preserve the type operations: $(\ph\meet\psi)[M/x] = (\ph[M/x] \meet \psi[M/x])$ and so on.
Thus, in the free structure built from type theory the reindexing functors do preserve all the relevant structure, so we can't hope for it to be initial except in a world where that structure is always preserved.

Of course, one may naturally wonder, where do indexed multiposets with these properties come from?
We will consider this question in more depth in \cref{sec:subobjects}, but here are three fundamental examples to help the intuition.

\begin{eg}\label{eg:subset-hyperdoctrine}
  Let $\cS=\bSet$ be the category of sets, and define $\cP(\Gamma)$ to be the poset of subsets of the set $\Gamma$, with its cartesian multiposet structure.
  The latter is in fact a Heyting algebra, and moreover a Boolean algebra: $\meet$ is intersection, $\join$ is union, $\neg$ is complement.
\end{eg}

\begin{eg}\label{eg:subobject-hyperdoctrine}
  Let \cS be any category with finite limits, and define $\cP(\Gamma)$ to be the poset of subobjects of $\Gamma$, i.e.\ isomorphism classes of monomorphisms with codomain $\Gamma$.
  The reindexing functors are given by pullback.
  When $\cS=\bSet$, this reproduces \cref{eg:subset-hyperdoctrine} up to isomorphism.
  In general, we need more structure on \cS to ensure that this \cP has the structure of \cref{defn:hyperdoctrine-heyting-fibers}; we will study this question in \cref{sec:subobjects}.
\end{eg}

\begin{eg}\label{eg:family-hyperdoctrine}
  Let $H$ be any complete Heyting algebra, let $\cS=\bSet$, and define $\cP(\Gamma) = H^\Gamma$, the poset of $\Gamma$-indexed families $\{h_i\}_{i\in\Gamma}$ of objects of $H$.
  The Heyting algebra operations on $H$ applied pointwise (e.g. $\{h_i\}_{i\in\Gamma} \meet \{k_i\}_{i\in\Gamma}= \{h_i\meet k_i\}_{i\in\Gamma}$) make $\cP(\Gamma)$ a Heyting algebra as well.
  Note that when $H=\tv$, this again reproduces \cref{eg:subset-hyperdoctrine} up to isomorphism.
\end{eg}

It remains to consider categorical analogues of the quantifiers and equality.
Lawvere's fundamental insight~\cite{lawvere:adjointness,lawvere:comprehension} was that these correspond categorically to \emph{adjoint functors}.

Consider, for instance, the universal quantifier.
We saw in \cref{sec:forall} that its rules could be given as the following pair:
\begin{mathpar}
  \inferrule{\Gamma,x:A\cb \Theta\types \ph}{\Gamma\cb\Theta\types \forall x:A.\ph}\;\forallI\and
  \inferrule{\Gamma\cb\Theta\types \forall x:A.\ph}{\Gamma,x:A\cb\Theta\types \ph}\;\forallI^{-1}
\end{mathpar}
which are clearly inverses to each other.
Categorically, they say that to have a morphism from $\Theta$ to $\forall x:A.\ph$ in $\cP(\Gamma)$ is equivalent to having a morphism from $\Theta$ to $\ph$ in $\cP(\Gamma,A)$.
Here the second $\Theta$ technically denotes the weakening of $\Theta$ to the context $\Gamma,x:A$, which categorically will be the functorial action of $\cP$ applied to the projection $(\Gamma,A)\to \Gamma$.
Note that the latter is one of the projections of a cartesian product in the category of contexts.
This leads to the following definition.

\begin{defn}\label{defn:multicat-radj}
  Let $F:\cM\to\cN$ be a functor of \fS-multicategories.
  We say it \textbf{has a right adjoint} if for each object $B\in\cN$ there is an object $GB\in\cM$ and a morphism $\ep_B:FGB\to B$ in \cN such that for any $A_1,\dots,A_n\in \cM$, the composite
  \[ \cM(A_1,\dots,A_n;GB) \xto{F} \cN(FA_1,\dots,FA_n;FGB) \xto{\ep_B\circ -} \cN(FA_1,\dots,FA_n;B) \]
  is a bijection.
\end{defn}

The case $n=1$ of this definition implies immediately that the underlying ordinary functor of $F$ has a right adjoint in the usual sense.
Conversely, in the case when \cM and \cN are representable, it is sufficient to have such an underlying adjoint together with the fact that $F$ preserves tensor products; see \cref{ex:moncat-radj}.
Moreover, if $G$ exists, it can be made into a functor $\cN\to\cM$, that is right adjoint to \cM in an appropriate 2-category of \fS-multicategories; see \cref{ex:multicat-radj}.

We need one more thing for a categorical analogue of $\all$: we need to know that this structure is ``preserved by the reindexing functors'' in an appropriate sense.
The appropriate sense is the following.

\begin{defn}\label{defn:bc}
  Let \cS be a category, let $\cP:\cS\op\to\bCat$ be a functor, and suppose we have a commutative square in \cS:
  \[ \xymatrix{ A \ar[r]^h \ar[d]_f & C \ar[d]^g \\ B \ar[r]_k & D. } \]
  Suppose furthermore that the functors $f^*:\cP(B) \to \cP(A)$ and $g^*:\cP(D) \to\cP(C)$ have right adjoints $f_*$ and $g_*$.
  We say that \cP satisfies the \textbf{right Beck--Chevalley condition} with respect to this square (or sometimes that the square satisfies the Beck-Chevalley condition with respect to \cP) if the composite natural transformation
  \[ k^* g_* \xto{\eta k^* g_*} f_* f^* k^* g_*  = f_* h^* g^* g_* \xto{f_* h^* \ep} f_* h^* \]
  is an isomorphism.
  Dually, if $f^*$ and $g^*$ have left adjoints $f_!$ and $g_!$, we say \cP satisfies the \textbf{left Beck--Chevalley condition} with respect to the above square if the composite
  \[ f_! h^* \xto{f_! h^* \eta} f_! h^* g^* g_! = f_! f^* k^* g_! \xto{\ep k^* g_!} k^* g_! \]
  is an isomorphism.
\end{defn}

When \cP is an \cS-indexed \fS-multiposet, we apply this definition to its underlying functor into posets (regarded as categories).
Since our posets are antisymmetric, every isomorphism is an equality, and so in this case we have $k^* g_* = f_* h^*$ (or $f_! h^* = k^* g_!$).
Now we can state:

\begin{defn}
  An \cS-indexed \fS-multiposet \textbf{has universal quantifiers} if
  \begin{enumerate}
  \item For any objects $\Gamma,A\in \cS$, the reindexing functor $\cP(\Gamma) \to \cP(\Gamma\times A)$ has a right adjoint in the sense of \cref{defn:multicat-radj}; and
  \item For any morphism $f:\Gamma\to\Delta$ and object $A$ in \cS, \cP satisfies the right Beck--Chevalley condition with respect to the square
    \[ \xymatrix@C=3pc{ \Gamma\times A \ar[r]^{f\times \idfunc_A} \ar[d] & \Delta\times A \ar[d] \\ \Gamma \ar[r]_f & \Delta. } \]
  \end{enumerate}
\end{defn}

Note that the Beck--Chevalley condition is true in the syntax because the universal quantifier is preserved by substitution, by definition of substitution: $(\forall x:A.\ph)[M/y] = \forall x:A. \ph[M/y]$ as long as $y\neq x$.
For the indexed poset of subsets from \cref{eg:subset-hyperdoctrine}, the right adjoint to $(\pi_A)^* : \cP(\Gamma) \to \cP(\Gamma\times A)$ is similarly defined by
\[ (\pi_A)_*(\ph) = \setof{ x\in \Gamma | \all y\in A. (x,y)\in\ph }. \]
Such right adjoints for \cref{eg:subobject-hyperdoctrine} will be studied in \cref{sec:heyting-categories}; while for \cref{eg:family-hyperdoctrine}, they can defined by
\[ (\pi_A)_*\left(\{h_{(i,a)}\}_{(i,a)\in\Gamma\times A}\right) = \left\{\bigwedge_a h_{(i,a)}\right\}_{i\in\Gamma} \]

The existential quantifier is similar, but a bit more subtle.
We saw in \cref{sec:exists} that its rules could be expressed as the pair
\begin{mathpar}
  \inferrule{\Gamma,x:A\cb\Theta,\ph\types \psi}{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}\;\existsL\and
  \inferrule{\Gamma\cb\Theta,(\exists x:A.\ph)\types \psi}{\Gamma,x:A\cb\Theta,\ph\types \psi}\;\existsL^{-1}\and
\end{mathpar}
which likewise seem to express some kind of adjunction; but there is an extra context $\Theta$ hanging around.
Translating directly across the correspondence to multicategories, this leads to the following definition.

\begin{defn}\label{defn:multicat-hopf-ladj}
  Let $G:\cM\to\cN$ be a functor of \fS-multicategories.
  We say it \textbf{has a Hopf left adjoint} if for each object $B\in\cN$ there is an object $FB\in\cM$ and a morphism $\eta:B\to GFB$ in \cN such that for any objects $A_1,\dots,A_n,C_1,\dots,C_m,D\in \cM$, the composite
  \[ \cM(\vec A,FB,\vec C;D) \xto{G} \cN(G\vec A, GFB, G\vec C; GD) \xto{-\circ_{(n+1)} \eta} \cN(G\vec A, B, G\vec C; GD) \]
  is a bijection.
\end{defn}

As before, the case $n=m=1$ implies that the underlying ordinary functor has a left adjoint in the usual sense.
Conversely, when \cM and \cN are representable and $G$ preserves tensor products, an underlying left adjoint is a Hopf left adjoint just when some canonical maps are isomorphisms; see \cref{ex:hopf-ladj}.
Unlike the case of right adjoints, however, in general a Hopf left adjoint cannot be made into a functor of multicategories.

\begin{defn}
  An \cS-indexed \fS-multiposet \textbf{has existential quantifiers} if
  \begin{enumerate}
  \item For any objects $\Gamma$ and $A$ of \cS, the reindexing functor $\cP(\Gamma) \to \cP(\Gamma\times A)$ has a Hopf left adjoint in the sense of \cref{defn:multicat-hopf-ladj}; and
  \item For any morphism $f:\Gamma\to\Delta$ and object $A$ in \cS, \cP satisfies the left Beck--Chevalley condition with respect to the square
    \[ \xymatrix@C=3pc{ \Gamma\times A \ar[r]^{f\times \idfunc_A} \ar[d] & \Delta\times A \ar[d] \\ \Gamma \ar[r]_f & \Delta. } \]
  \end{enumerate}
\end{defn}

Unsurprisingly, for the indexed poset of subsets from \cref{eg:subset-hyperdoctrine}, the left adjoint to $(\pi_A)^*:\cP(\Gamma) \to \cP(\Gamma\times A)$ is similarly defined by
\[ (\pi_A)_!(\ph) = \setof{ x\in \Gamma | \exis y\in A. (x,y)\in\ph }. \]
Left adjoints for \cref{eg:subobject-hyperdoctrine} will be studied in \cref{sec:regular-categories}, while those in \cref{eg:family-hyperdoctrine} can be defined like the right adjoints using joins instead of meets:
\[ (\pi_A)_!\left(\{h_{(i,a)}\}_{(i,a)\in\Gamma\times A}\right) = \left\{\bigvee_a h_{(i,a)}\right\}_{i\in\Gamma} \]

Finally, we consider the rules for equality:
\begin{mathpar}
  \inferrule{ }{\Gamma,x:A\cb \ec\types (x=_A x)}\and
  \inferrule{\Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]}{\Gamma,x:A,y:A\cb\Theta,(x=_A y)\types \ph}
\end{mathpar}
Although we didn't mention it in \cref{sec:equality}, the first of these rules is equivalent to the opposite of the second, similarly to what happened for the quantifiers.
One direction is immediate:
\begin{mathpar}
  \inferrule*{\inferrule*{ }{\Gamma,x:A,y:A\cb(x=_A y)\types (x=_A y)}}{\Gamma,x:A\cb\ec\types (x=_A x)}
\end{mathpar}
while the other uses a cut and a substitution:
\begin{mathpar}
  \inferrule*[right=cut]{
    \inferrule*{ }{\Gamma,x:A \cb \ec \types x=_A x}\\
    \inferrule*[Right=subst $x/y$]{\Gamma,x:A,y:A\cb\Theta,(x=_A y)\types \ph}
    {\Gamma,x:A\cb\Theta[x/y],(x=_A x)\types \ph[x/y]}
  }{\Gamma,x:A\cb\Theta[x/y]\types \ph[x/y]}
\end{mathpar}

Thus, what we have looks very much like a (Hopf) left adjoint to substitution along the diagonal $(\Gamma,A) \to (\Gamma,A,A)$ in the category of contexts; but there is \emph{no} proposition in context $(\Gamma,A)$ that it is applied to.
This suggests the following definitions.

\begin{defn}\label{defn:multicat-hopf-ladj-empty}
  Let $G:\cM\to\cN$ be a functor of \fS-multicategories.
  We say it \textbf{has a Hopf left adjoint at $()$} if there is an object $F\in\cM$ and a morphism $\eta:()\to GF$ in \cN such that for any objects $A_1,\dots,A_n,C_1,\dots,C_m,D\in \cM$, the composite
  \[ \cM(\vec A,F,\vec C;D) \xto{G} \cN(G\vec A, GF, G\vec C; GD) \xto{-\circ_{(n+1)} \eta} \cN(G\vec A, G\vec C; GD) \]
  is a bijection.
\end{defn}

\begin{defn}
  Suppose given an \cS-indexed \fS-multiposet \cP and a commutative square in \cS:
  \[ \xymatrix{ A \ar[r]^h \ar[d]_f & C \ar[d]^g \\ B \ar[r]_k & D, } \]
  and suppose that the reindexing functors $f^*$ and $g^*$ have Hopf left adjoints at $()$, given by objects $f_!\in \cP(B)$ and $g_!\in \cP(D)$.
  Then there is a unique morphism $f_! \to k^* g_!$ in $\cP(B)$ such that the composite $() \xto{\eta} f^* f_! \to f^* k^* g_!$ in $\cP(A)$ is equal to the composite $() \xto{h^* \eta} h^* g^* g_!$ (note $f^* k^* = h^* g^*$).
  We say that \cP satisfies the \textbf{left Beck--Chevalley condition at $()$} with respect to this square if this morphism $f_! \to k^* g_!$ is an isomorphism.
\end{defn}

\begin{defn}
  An \cS-indexed \fS-multiposet with unit objects \textbf{has equality} if
  \begin{enumerate}
  \item For any objects $\Gamma$ and $A$ of \cS, the reindexing functor $\cP(\Gamma\times A\times A) \to \cP(\Gamma\times A)$ has a Hopf left adjoint at $()$; and
  \item For any morphism $f:\Gamma\to\Delta$ and object $A$ in \cS, \cP satisfies the left Beck--Chevalley condition at $()$ with respect to the square
    \[ \xymatrix@C=5pc{ \Gamma\times A \ar[r]^{f\times \idfunc_A} \ar[d] & \Delta\times A \ar[d] \\
      \Gamma\times A\times A \ar[r]_{f\times \idfunc_A \times \idfunc_A} & \Delta\times A\times A. } \]
  \end{enumerate}
\end{defn}

As before, the Beck--Chevalley condition is true in the syntax because ``equality is preserved by substitution''.
The relevant substitution here is not the one built into the equality rule, though, but the substitution for different variables, which doesn't change the equality proposition at all: $(x=_A y)[M/z] = (x=_A y)$ as long as $z\neq x$ and $z\neq y$.
For the indexed poset of subsets from \cref{eg:subset-hyperdoctrine}, the left adjoint to $(\Delta_A)^* : \cP(\Gamma\times A\times A) \to \cP(\Gamma\times A)$ at $()$ is defined by
\[ (\Delta_A)_! = \setof{ (i,x,y)\in \Gamma\times A\times A | x=y }. \]
Left adjoints in \cref{eg:subobject-hyperdoctrine} actually always exist (see \cref{thm:horn-subobjects}), while those in \cref{eg:family-hyperdoctrine} can be defined by
\[ ((\Delta_A)_!)_{(i,x,y)\in \Gamma\times A\times A} =
\begin{cases}
  \top &\text{if } x=y\\
  \bot &\text{if } x\neq y.
\end{cases}
\]

Note that we are sticking doggedly to the principle that just as the rules for a given type operation should be independent of any other type operations, the corresponding universal property should be statable without reference to any other objects with universal properties.\footnote{At least, other universal properties in the multiposets $\cP(\Gamma)$.
We do still refer to cartesian products in \cS, but we could also remove those by working with ``presheaves on multicategories'' as sketched at the beginning of this section.}
If we \emph{do} have additional structure, particularly tensor products and units in the multiposets $\cP(\Gamma)$, then our various kinds of adjoints can be formulated in terms of those and ordinary adjunctions --- see \cref{ex:multicat-radj,ex:moncat-radj,ex:hopf-ladj,ex:hopf-ladj-at-one} --- and our examples in \cref{sec:subobjects} will mainly arise in this way.
However, to make a closer connection to the type theory we prefer to formulate them independently first.

\begin{defn}
  A \textbf{first-order \fS-hyperdoctrine} consists of a category \cS with finite products together with an \cS-indexed \fS-multiposet that is closed and representable and has products (finite meets), coproducts (finite joins), universal and existential quantifiers, and equality.

  By default, a \textbf{first-order hyperdoctrine} refers to the cartesian case where $\fS$ contains all functions; in this case representability is equivalent to having finite meets.
  More generally, an \cS-indexed cartesian multiposet is called a:
  \begin{enumerate}
  \item \textbf{coherent hyperdoctrine} if it has finite meets, finite joins, existential quantifiers, and equality;
  \item \textbf{geometric hyperdoctrine} if it has finite meets, infinite joins, existential quantifiers, and equality;
  \item \textbf{regular hyperdoctrine} if it has finite meets, existential quantifiers, and equality; and a
  \item \textbf{Horn hyperdoctrine} if it has finite meets and equality.
  \end{enumerate}
\end{defn}

Note that since all the structure of a first-order \fS-hyperdoctrine is determined by universal properties, it is unique up to isomorphism, and hence unique on the nose in an (antisymmetric) poset.
Thus, there is no need to suppose separately that we have \emph{chosen} such operations.

\begin{thm}\label{thm:fol-initial}
  The free first-order \fS-hyperdoctrine generated by a first-order \fS-theory can be presented, up to equivalence, by the type theory of the latter:
  \begin{itemize}
  \item \cS is the category of type contexts; and
  \item the poset $\cP(\Gamma)$ is obtained from the poset of proposition judgments $\Gamma\types \ph\prop$ and derivable entailments $\Gamma\cb\Theta\types\ph$ by identifying isomorphic objects (since in this section our posets are antisymmetric).
  \end{itemize}
  (And similarly for the other fragments with fewer type operations.)
\end{thm}
\begin{proof}
  We have already observed that this structure defines an indexed \fS-multicategory and that the simple type operations $\meet,\top,\join,\bot,\tensor,\one,\hom$ yield the appropriate multicategorical strurcture.
  Moreover, we defined the categorical notions of universal and existential quantifiers and equality precisely so that they would hold in the syntax; thus the description above does yield a first-order \fS-hyperdoctrine.

  Now, the underlying multigraph of a first-order \fS-theory is of course a finite-product theory without axioms, and we showed in \cref{sec:fp-theories} that the category of contexts of its type theory is, up to equivalence, the free category with products it generates.
  Thus, it maps uniquely (up to isomorphism) into the base category of any other first-order \fS-hyperdoctrine; it remains to show that this map extends uniquely to a map of hyperdoctrines, i.e.\ a natural transformation between the $\cP$-functors preserving all the structure.

  As usual, we do this by induction on derivations.
  The proposition judgment $\Gamma\types \ph\prop$ is easy: each rule corresponds to one of the objects with a universal property that we have assumed to exist in any first-order \fS-hyperdoctrine.
  Next, since the rules for entailment involve substitution of terms into propositions, before defining our functor on entailments we have to first prove that it maps such substitutions to the reindexing functors in the target; this is another straightforward induction on derivations of $\Gamma\types \ph\prop$.
  Now the rules for entailment involving simple type operations are also easy, just as in \cref{sec:logic}.
  Finally, in \crefrange{sec:forall}{sec:equality} and this section we showed that the natural deduction rules for quantifiers and equality are inter-derivable (in the presence of substitution and cut) with the rules that exactly express the appropriate kind of adjunctions.

  This completes the definition on entailments.
  Since everything is posetal there is not much left to do: we show that our map preserves all the hyperdoctrine structure, essentially by definition, and then that it is unique (modulo the up-to-isomorphism uniqueness of the functor on base categories), because its definition was forced at every step.
\end{proof}

\begin{rmk}\label{rmk:fol-soundness-completeness}
  As noted in \cref{rmk:soundness-completeness} for propositional logic, \cref{thm:fol-initial} implies the traditional \emph{soundness} and \emph{completeness} theorems for first-order logic with respect to hyperdoctrines.
  The soundness theorem says that if we can prove $\Gamma\cb \ec\types \ph$, then when we interpret our logic into any hyperdoctrine, $\ph$ must go to the top element, i.e.\ it must ``be true''.
  In particular, this applies to models in the hyperdoctrine of sets and subsets from \cref{eg:subset-hyperdoctrine}, which are the classical notion of ``model''.
  (In \cref{sec:subobjects} we will construct hyperdoctrines from more general categories than \bSet.)
  Conversely, the completeness theorem says that if something is true in all hyperdoctrines, then it must in particular be true in the free one constructed from the type theory, and therefore must be provable in the type theory.
\end{rmk}

\begin{rmk}
  Note that all categorical structure corresponding to quantifiers and equality takes the form of \emph{certain} adjoints to reindexing functors.
  As we will see in \cref{sec:subobjects}, most examples arising in practice naturally have adjoints to \emph{all} the reindexing functors (if they have any).
  However, this is not actually an additional condition; given only the adjoints assumed in our definition of first-order hyperdoctrine, we can \emph{construct} adjoints to arbitrary reindexing functors and \emph{prove} that they satisfy some Beck--Chevalley conditions.
  At the moment, we leave this proof to the reader; see \cref{ex:hyperdoctrine-alladj}.
  (In fact, it is more usual to include all such adjoints, and their Beck--Chevalley conditions, in the definition of ``hyperdoctrine''.)
  % TODO: Do the construction of adjoints, at least, here as an example; let the reader check BC.
  % Note that we do something like this in a special case later on, in \cref{thm:regular-subobjects,thm:heyting-subobjects,ex:reg-allbc}.  Can we connect them up?
\end{rmk}


\subsection*{Exercises}

\begin{ex}\label{ex:pshf-multi-catprod}
  Prove \cref{thm:pshf-multi-catprod}.
\end{ex}

\begin{ex}\label{ex:multicat-radj}
  Suppose a functor $F:\cM\to\cN$ of \fS-multicategories has a right adjoint in the sense of \cref{defn:multicat-radj}.
  \begin{enumerate}
  \item Prove that if \cM and \cN are both representable, then $F$ preserves tensor products in the sense of \cref{ex:mcat-strong-func}.
  \item Extend $G$ to a functor $G:\cN\to\cM$.
  \item Define a 2-category of \fS-multicategories and show that $G$ is right adjoint to $F$ in this 2-category (i.e.\ there are 2-cells $\eta : 1 \to G F$ and $\ep : F G \to 1$ in this 2-category satisfying the triangle identities).
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:moncat-radj}
  Let \cM and \cN be representable \fS-multicategories.
  Prove that a functor $F:\cM\to\cN$ has a right adjoint in the sense of \cref{defn:multicat-radj} if and only if (1) it preserves tensor products in the sense of \cref{ex:mcat-strong-func} and (2) its underlying ordinary functor has a right adjoint.
\end{ex}

\begin{ex}\label{ex:multicat-prod-ladj}
  Show that an \fS-multicategory \cM has binary products, in the sense defined before \cref{thm:multicat-prod}, if and only if the diagonal $\cM\to \cM\times \cM$ has a right adjoint in the sense of \cref{defn:multicat-radj}.
\end{ex}

\begin{ex}\label{ex:beck-chev}
  Let $\cP:\cS\op\to\bCat$ and suppose we have a commutative square in \cS:
  \[ \xymatrix{ A \ar[r]^h \ar[d]_f & C \ar[d]^g \\ B \ar[r]_k & D. } \]
  such that $f^*$ and $g^*$ have left adjoints and also $h^*$ and $k^*$ have right adjoints.
  Prove that \cP satisfies the left Beck-Chevalley condition with respect to this square if and only if it satisfies the right Beck--Chevalley condition with respect to the transposed square
  \[ \xymatrix{ A \ar[r]^f \ar[d]_h & B \ar[d]^k \\ C \ar[r]_g & D. } \]
\end{ex}

\begin{ex}\label{ex:hopf-ladj}
  Let \cM and \cN be representable \fS-multicategories, and $G:\cM\to\cN$ a functor preserving tensor products.
  \begin{enumerate}
  \item Show that $G$ has a Hopf left adjoint if and only if its underlying ordinary functor has a left adjoint $F$ such that the canonical map
    \begin{gather*}
      F(A\tensor G B) \to F(G F A \tensor G B) \toiso F G(F A \tensor B) \to F A \tensor B
    \end{gather*}
    is an isomorphism for any $A\in\cN$ and $B\in \cM$.
  \item If \cM and \cN are additionally closed, and $G$ is also closed in the sense that the canonical maps $G(A\hom B) \to G A \hom G B$ are isomorphisms, prove that $g$ has a Hopf left adjoint if and only if its underlying ordinary functor has a left adjoint.
  % TODO: If $G$ is not assumed to preserve tensor products, does a "Hopf left adjoint" in the multicategory sense imply a Hopf adjunction in the monoidal category sense?
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:multicat-coprod-ladj}
  Show that an \fS-multicategory \cM has binary coproducts, in the sense defined before \cref{thm:multicat-coprod}, if and only if the diagonal $\cM\to \cM\times \cM$ has a Hopf left adjoint.
\end{ex}

\begin{ex}\label{ex:hopf-ladj-at-one}
  Let \cM and \cN be \fS-multicategories, let $G:\cM\to\cN$ be a functor having a Hopf left adjoint, and assume that \cN has a unit object.
  Prove that $G$ also has a Hopf left adjoint at $()$.
\end{ex}

\begin{ex}\label{ex:hyperdoctrine-alladj}
  Suppose $\cP:\cS\op\to\mathbf{Heyt}$ is a first-order \fS-hyperdoctrine as defined in the text.
  \begin{enumerate}
  \item Prove (using type theory or commutative diagrams, your choice) that in fact the reindexing functor $f^* : \cP(\Delta) \to \cP(\Gamma)$ has a Hopf left adjoint for \emph{all} morphisms $f:\Gamma\to\Delta$ in $\cS$.
    \textit{(Hint: in the hyperdoctrine of subsets over $\mathbf{Set}$, these left adjoints can be defined by $f_!(\varphi) = \setof{ y\in \Delta | \exis x\in \Gamma. (x\in\varphi\meet f(x) = y) }$.)}
  \item Similarly, prove that $f^*$ has a right adjoint for all $f$.
  \item Prove that these left adjoints satisfy both Beck--Chevalley conditions for commutative squares of the following form:
    \[
    \xymatrix@C=3pc{ A \ar[r]^-{(1,f)} \ar[d]_{f} & A\times B \ar[d]^{f\times 1} \\ B \ar[r]_-{\Delta} & B\times B }\hspace{2cm}
    \xymatrix@C=3pc{A \ar[r]^-\Delta \ar[d]_\Delta & A\times A \ar[d]^{1\times \Delta} \\ A\times A \ar[r]_-{\Delta\times 1} & A\times A\times A}
    \]
  \end{enumerate}
\end{ex}


\section{Hyperdoctrines of subobjects}
\label{sec:subobjects}

Finally, we turn to the question of where hyperdoctrines come from.
From now on we will focus entirely on the cartesian monoidal case (with all the structural rules), which is the most-studied and most-applicable.

\subsection{Horn hyperdoctrines from finite limits}
\label{sec:horn-subobjects}

\cref{eg:subset-hyperdoctrine} suggests that from a category \cS, we should try to construct a hyperdoctrine such that for $\Gamma\in\cS$, $\cP(\Gamma)$ is a poset of ``subobjects'' of $\Gamma$.
Moreover, there is a standard way to define a subobject of $\Gamma$, namely as an isomorphism class of monomorphisms with target $\Gamma$.

We write this poset as $\sub_\cS(\Gamma)$, or just $\sub(\Gamma)$.
To make $\sub_\cS$ into an \cS-indexed poset in a natural way, we need \cS to have pullbacks of monomorphisms along arbitrary morphisms.
However, a category with finite products and pullbacks of monomorphisms automatically has all finite \emph{limits}, since the equalizer of $f,g:A\to B$ can be constructed as the pullback of the monomorphism $\Delta:B\to B\times B$ along $(f,g):A\to B\times B$.

Thus, \emph{from now on we assume that \cS has finite limits}, so that $\sub_\cS$ is an \cS-indexed poset (which we already mentioned in \cref{eg:subobject-hyperdoctrine}).
Moreover this \cS-indexed poset has products (meets) and a terminal (greatest) object; the former are given by pullback of monomorphisms (which we henceforth call \emph{intersections}) and the latter by the monomorphism $\idfunc_\Gamma : \Gamma \to \Gamma$.
We can also show:

\begin{thm}\label{thm:horn-subobjects}
  If \cS has finite limits, then $\sub_\cS$ has equality.
  Therefore, it is a Horn hyperdoctrine.
\end{thm}
\begin{proof}
  For any objects $\Gamma$ and $A$, the diagonal $1\times \Delta : \Gamma\times A \to \Gamma\times A\times A$ is itself a monomorphism, so we can regard it as a subobject of $\Gamma\times A\times A$.
  For this to give the desired Hopf left adjoint at $()$, we must show that for any monomorphisms $\Theta \mono \Gamma\times A\times A$ (being the intersection of some number of subobjects) and $C \mono \Gamma\times A\times A$, we have $\Theta \cap (\Gamma\times A) \le C$ as subobjects of $\Gamma\times A\times A$ if and only if we have $(1\times \Delta)^* \Theta \le (1\times \Delta)^* C$ as subobjects of $\Gamma\times A$.
  However, $\Theta \cap (\Gamma\times A)$ and $(1\times \Delta)^* \Theta$ are the same object, and so this bijection is just using the universal property of the pullback $(1\times \Delta)^* C$:
  \[ \xymatrix{ (1\times \Delta)^* \Theta \ar@(r,ul)[drr] \ar@(d,ul)[ddr] \ar@{.>}[dr] \\
    & (1\times \Delta)^* C \ar[d] \ar[r] & C \ar[d]\\
    & \Gamma\times A \ar[r]_-{1\times\Delta} & \Gamma\times A\times A } \]
  Finally, we have a pullback square:
  \[ \xymatrix{ \Gamma\times A \ar[r] \ar[d] & \Delta\times A \ar[d] \\
    \Gamma\times A\times A \ar[r]_{f\times 1\times 1} & \Delta\times A\times A } \]
  which implies the Beck--Chevalley condition.
\end{proof}

Therefore, any Horn theory can be interpreted into any category with finite limits.
(In fact, more than this can be done in categories with finite limits, but it is slightly tricky to characterize exactly what; we will come back to this in \cref{sec:lex-theories}.)


\subsection{Regular categories}
\label{sec:regular-categories}

Now we move on to regular logic.
For $\sub_\cS$ to have existential quantifiers, we need some way to make a subobject $C\mono \Gamma\times A$ into a subobject of $\Gamma$.
In $\sub_\bSet$, the desired subset of $\Gamma$ is the \emph{image} of the composite function $C\mono \Gamma\times A \to\Gamma$, so it seems natural to consider categories that have a well-behaved notion of ``image factorization''.

\begin{defn}
  An \textbf{extremal epimorphism} is a morphism $e:A\to B$ in a category such that if $e = m g$ with $m$ a monomorphism, then $m$ is an isomorphism.
  A \textbf{regular category} is a category with finite limits such that every morphism $f$ factors as $m e$ where $m$ is a monomorphism and $e$ an extremal epimorphism, and moreover extremal epimorphisms are stable under pullback.
\end{defn}

We start with a lemma about extremal epimorphisms:

\begin{lem}\label{thm:extremal-epi}
  Let \cS be a category with finite limits.
  \begin{enumerate}
  \item Every extremal epimorphism is an epimorphism.\label{item:ee1}
  \item If we have a commutative square in \cS
    \[ \xymatrix{ A \ar[r] \ar[d]_e & C \ar[d]^m \\ B \ar[r] & D} \]
    in which $e$ is an extremal epimorphism and $m$ a monomorphism, there exists a unique morphism $B\to C$ making both triangles commute.
    (This means, by definition, that $e$ is also a \textbf{strong epimorphism}.)\label{item:ee2}
  \item If a morphism $f$ in \cS factors as $m e$ with $e$ an extremal epi and $m$ a monomorphism, then such a factorization is unique up to isomorphism.\label{item:ee3}
  \end{enumerate}
\end{lem}
\begin{proof}
  For~\ref{item:ee1}, if $e$ is extremal epi and $f e = g e$, then the equalizer of $f$ and $g$ is a monomorphism through which $e$ factors; so it is an isomorphism and thus $f=g$.

  For~\ref{item:ee2}, the projection $B\times_D C \to B$ is a monomorphism through which $e$ factors, so it is an isomorphism.
  The composite $B\to B\times_D C \to C$ is then the desired morphism; its uniqueness follows from the fact that $m$ is mono.

  For~\ref{item:ee3}, two such factorizations give a squares as in~\ref{item:ee2} whose transpose is also such a square, so it has diagonal fillers in both directions, giving inverse isomorphisms.
\end{proof}

\begin{thm}\label{thm:regular-subobjects}
  A category \cS with finite limits is regular if and only if $\sub_\cS$ has existential quantifiers.
\end{thm}
\begin{proof}
  First suppose \cS is regular, and that we have a subobject $\ph\mono \Gamma\times A$.
  Factor the composite $\ph \mono \Gamma\times A \to \Gamma$ as an extremal epi $\ph \to \exis_A \ph$ followed by a mono $\exis_A \ph \mono \Gamma$.
  Then we must show that given any other monos $\Theta \mono \Gamma$ and $\psi\mono \Gamma$, we have $\Theta \cap \exis_A \ph \le \psi$ if and only if $(\pi_A)^*\Theta \cap \ph \le (\pi_A)^* \psi$.
  Now by the functoriality of pullback, we have a diagram:
  \[ \xymatrix{ (\pi_A)^*\Theta \cap \ph \ar[dd] \ar[dr] \ar[rr] && \Theta \cap \exis_A \ph \ar'[d][dd] \ar[dr] \\
    & \ph \ar[dd] \ar[rr] && \exis_A \ph \ar[dd]\\
    (\pi_A)^*\Theta \ar[dr] \ar'[r][rr] && \Theta \ar[dr] \\
    & \Gamma\times A \ar[rr]_{\pi_A} && \Gamma. } \]
  Thus in one direction, if $\Theta \cap \exis_A \ph \le \psi$, we have a composite map $(\pi_A)^*\Theta \cap \ph \to \psi$ over $\Gamma$, which induces a map $(\pi_A)^*\Theta \cap \ph \le (\pi_A)^* \psi$ by the universal property of pullback $(\pi_A)^*$.
  And in the other direction, if $(\pi_A)^*\Theta \cap \ph \le (\pi_A)^* \psi$, we have a square
  \[ \xymatrix{ (\pi_A)^*\Theta \cap \ph \ar[r]  \ar[d] & (\pi_A)^* \psi \ar[r] & \psi \ar[d] \\
    \Theta \cap \exis_A \ph \ar[rr] && \Gamma } \]
  as in \cref{thm:extremal-epi}\ref{item:ee2}.
  (The fact that the left-hand arrow is an extremal epi uses the assumption on a regular category that pullback preserves extremal epis.)
  Thus there is a diagonal filler giving $\Theta \cap \exis_A \ph \le \psi$.

  For the Beck--Chevalley condition, if we have $f:\Gamma\to\Delta$ and a mono $\ph\mono \Delta\times A$, by pasting pullback squares we see that the outer rectangle below is a pullback:
  \[ \xymatrix{ (f\times \idfunc_A)^*\ph \ar[d]\ar[r] & \ph \ar[d] \\
    \Gamma\times A \ar[r]^{f\times \idfunc_A}\ar[d] & \Delta\times A \ar[d] \\
    \Gamma \ar[r]_f & \Delta } \]
  Now if we pull back the factorization $\ph \to \exis_A \ph \to \Delta$ along $f$ we get another pair of pullback squares
  \[ \xymatrix{ (f\times \idfunc_A)^*\ph \ar[d]\ar[r] & \ph \ar[d] \\
    f^*(\exis_A \ph) \ar[r]^{f\times \idfunc_A}\ar[d] & \exis_A \ph \ar[d] \\
    \Gamma \ar[r]_f & \Delta. } \]
  Since monos and extremal epis are both stable under pullback, the left-hand maps form a factorization of the map $(f\times \idfunc_A)^*\ph \to \Gamma$; and since such factorizations are unique by \cref{thm:extremal-epi}\ref{item:ee3}, we must have $f^*(\exis_A \ph) \cong \exis_A ((f\times\idfunc_A)^*\ph)$, which is what the Beck--Chevalley condition requires.

  Now suppose \cS has finite limits and $\sub_\cS$ has existential quantifiers.
  Given a morphism $f:A\to B$, its ``graph'' $(f,1) : A\to B\times A$ is a monomorphism.
  Applying the existential quantifier for the projection $\pi_A:B\times A\to B$, we obtain a monomorphism $\exis(f,1) : C\mono B$ with the property that $\exis(f,1) \le D$ as subobjects of $B$ if and only if $(f,1) \le (\pi_A)^*D$ as subobjects of $B\times A$.
  By the universal property of pullback, the latter is equivalent to there being a map $A\to D$ such that the composite $A\to D \to B$ is equal to the composite $A \to B\times A \to B$; but the latter is $f$, so this just means that $f$ factors through $D$.

  In particular, since $\exis(f,1) \le \exis(f,1)$, it follows that $f$ factors through it, by some map $e:A\to \exis(f,1)$, say.
  Moreover, if we have a monomorphism $D\mono \exis(f,1)$ that $e$ factors through, then $f$ factors through the composite mono $D\to B$, and thus $\exis(f,1)\le D$ as subobjects of $B$; hence $D\cong \exis(f,1)$.
  Thus, $e$ is extremal epic, and so $A \xto{e} \exis(f,1) \to B$ is a factorization of $f$ as required in the definition of regular category.

  The uniqueness of factorizations means that if $f$ itself is extremal epic, then $\exis(f,1) \to B$ is an isomorphism.
  And of course, conversely, if $\exis(f,1) \to B$ is an isomorphism, then $f$, like $e$, is extremal epic.
  Now the Beck--Chevalley condition for existential quantifiers implies that the construction of $\exis(f,1)$ is preserved by pullback.
  Thus so is the property of $\exis(f,1) \to B$ being an isomorphism, and thus so is the property of $f$ being extremal epic.
  Therefore, $\cS$ is a regular category.
\end{proof}

Regular categories are quite common.
Of course, $\bSet$ is regular.
So is any presheaf category; and, as we will see later, so is any ``elementary topos''.
Moreover, the category of models of any finite-product theory (like monoids, groups, rings, etc.)\ is also regular; see \cref{ex:regular-egs}.
Thus, regular logic can be used to reason about any such category.

In fact, regular logic is quite useful in proving basic facts about regular categories.
To get started, we make the following observations.

\begin{lem}\label{thm:logic-extremal-epi}
  Consider the regular theory with two types $A,B$, one morphism $f:A\to B$, and one axiom $y:B \cb \ec \types \exists x:A.f(x)= y$.
  A model of this theory in a regular category \cS is precisely an extremal epimorphism in \cS.
\end{lem}
\begin{proof}
  By the proof of \cref{thm:regular-subobjects}, we can construct the interpretation of $y:B\types (\exists x:A.f(x)= y)\prop$ as follows:
  \begin{enumerate}
  \item Start with the diagonal $B\to B\times B$, for $y_1:B,y_2:B\types (y_1= y_2)\prop$.
  \item Pull it back along $(f\times \idfunc):A\times B\to B\times B$, representing the substitution $x:A,y:B\types (f(y)= y)\prop$.
    This yields the graph $(f,1):A\to A\times B$.
  \item Take the image of the composite $A\to A\times B \to B$.
    This composite is just $f$, so its image is also the image of $f$.
  \end{enumerate}
  Therefore, to interpret $y:B \cb \ec \types \exists x:A.f(x)= y$ is to say that the image of $f$ is all of $B$, i.e.\ that $f$ is extremal epic.
\end{proof}

The next lemma requires only Horn logic, but there was not much point to stating it before now.

\begin{lem}\label{thm:logic-mono}
  Consider the Horn theory with two types $A,B$, one morphism $f:A\to B$, and one axiom $x_1:A,x_2:A \cb (f(x_1)=f(x_2)) \types x_1=x_2$.
  A model of this theory in a category with finite limits is precisely a monomorphism.
\end{lem}
\begin{proof}
  The interpretation of $x_1:A,x_2:A \types (f(x_1)=f(x_2))\prop$ is the pullback of the diagonal $B\to B\times B$ along $f\times f$.
  This is otherwise known as the \emph{kernel pair} of $f$, namely the pullback of $f$ along itself.
  Thus, the axiom of our theory says pricely that this kernel pair is contained in the diagonal of $A$ (as a subobject of $A\times A$).
  Now if we have $h,k:X\to A$ such that $f h = f k$, then $(h,k)$ factors through the kernel pair; hence it also factors through the diagonal, which means $h=k$; so $f$ is monic.
\end{proof}

Our third lemma starts to reveal some of the real value of the logical approach.

\begin{lem}\label{thm:logic-uniquechoice}
  Suppose we have a regular theory containing two types $A,B$ and a proposition (not necessarily an atomic one) $x:A,y:B\types \ph\prop$ such that the following sequents are provable:
  \begin{mathpar}
    x:A \cb \ec \types \exists y:B.\ph\and
    x:A,y_1:B,y_2:B \cb \ph[y_1/y], \ph[y_2/y] \types y_1=y_2
  \end{mathpar}
  Then for any interpretation of this theory in a regular category, the interpretation of $\ph$ is a monomorphism $\ph \mono A\times B$ such that the composite $\ph \to A\times B \to A$ is an isomorphism; hence the composite $A\cong \ph \to A\times B \to B$ defines a morphism from $A$ to $B$.
\end{lem}
\begin{proof}
  Let us consider what the two assumptions say.
  By construction of $\exis$, the first says that the image of $\ph \to A\times B \to A$ is all of $A$, which is to say that this composite is extremal epi.

  The second says that if we pull $\ph \to A\times B$ back along the two projections $\pi_1,\pi_2 :A\times B\times B \toto A\times B$, then the intersection $(\pi_1)^*\ph \cap (\pi_2)^*\ph$ lies inside the diagonal $\Delta : A\times B \to A\times B\times B$.
  We claim this means that the composite $\ph \to A\times B \to A$ is mono.
  For if we have $f,g:X\to \ph$ that are equalized in $A$, we have an induced map $X \to A\times B\times B$ that factors through $(\pi_1)^*\ph \cap (\pi_2)^*\ph$.
  Hence it also factors through $\Delta$, which is to say that the two composites $X \toto \ph \to A\times B$ are equal; but since $\ph\mono A\times B$ is mono, this implies $f=g$.

  Thus, $\ph \to A\times B \to A$ is both extremal epi and mono.
  But since it factors through itself, this implies it is an isomorphism.
\end{proof}

We leave the proof of the final lemma to the reader (\cref{ex:logic-uniquechoice-funct}).

\begin{lem}\label{thm:logic-uniquechoice-funct}\ 
  \begin{enumerate}
  \item If in \cref{thm:logic-uniquechoice} the proposition $\ph$ is $f(x)=y$ for some morphism $f:A\to B$ in the theory, then the morphism $A\to B$ defined by \cref{thm:logic-uniquechoice} is just the interpretation of $f$.
  \item If in a regular theory we have three types $A,B,C$ and propositions
    \begin{mathpar}
      x:A,y:B\types \ph\prop\and
      y:B,z:C\types \psi\prop\and
      x:A,z:C\types \chi\prop\and
    \end{mathpar}
    all satisfying the hypotheses of \cref{thm:logic-uniquechoice}, and moreover we can prove
    \begin{mathpar}
      x:A,y:B,z:C \cb \ph,\psi \types \chi
    \end{mathpar}
    then under interpretation in any regular category, the induced morphisms $A\to B$ and $B\to C$ compose to the induced morphism $A\to C$.\qed
  \end{enumerate}
\end{lem}

Putting all these lemmas together, we can prove a nontrivial theorem about regular categories.

\begin{thm}\label{thm:logic-extepi-regepi}
  In a regular category, every extremal epi is in fact a regular epi (the coequalizer of some parallel pair).
\end{thm}
\begin{proof}
  We will show that every extremal epi is the coequalizer of its kernel pair.
  Note that since an extremal epi is epi by \cref{thm:extremal-epi}\ref{item:ee1}, factorizations through it are unique if they exist.
  Now, given $f:A\to B$ and $g:A\to C$, we can say that $g$ coequalizes the kernel pair of $f$ if and only if the kernel pair of $f$ is contained in the kernel pair of $g$ as a subobject of $A\times A$.

  Thus, consider the regular theory with three types $A,B,C$, two morphisms $f:A\to B$ and $g:A\to C$, and the axioms
  \begin{mathpar}
    y:B \cb \ec \types \exists x:A.f(x)= y\and
    x_1:A,x_2:A \cb (f(x_1)=f(x_2)) \types (g(x_1)=g(x_2))
  \end{mathpar}
  The first says exactly that $f$ is extremal epi, while the second says that the kernel pair of $f$ is contained in the kernel pair of $g$.
  In this theory, define $\ph$ to be the proposition
  \[y:B,z:C \types \exists x:A.((f(x)=y) \meet (g(x)=z)) \prop\]
  We will prove the following sequents in this theory:
  \begin{enumerate}
    \item $y:B \cb \ec \types \exists z:C.\ph$\label{item:eere1}
    \item $y:B,z_1:C,z_2:C \cb \ph[z_1/z], \ph[z_2/z] \types z_1=z_2$\label{item:eere2}
    \item $x:A,y:B,z:C \cb \ph, (f(x)=y) \types (g(x)=z)$\label{item:eere3}
  \end{enumerate}
  Then by \cref{thm:logic-uniquechoice,thm:logic-uniquechoice-funct}, the interpretation of $\ph$ will define a morphism $B\to C$ that factors $g$ through $f$.
  \begin{enumerate}
  \item Informally, suppose $y:B$.
    By one of our axioms, there exists an $x:A$ such that $f(x)=y$.
    Let $z=g(x)$; then of course $f(x)=y$ and $g(x)=z$.
    \begin{figure}
      \centering
      \[\tiny
      \inferrule*[Right=\tiny$\existsE$]{
        \mathrm{(axiom)} \\
        \inferrule*[Right=\tiny$\existsI$]{
          g(x):C\\
          \inferrule*[Right=\tiny$\existsI$]{
            \inferrule*[Right=\tiny$\meetI$]{
              \inferrule*{ }{y:B,x:A \cb (f(x)=y) \types (f(x)=y)}\\
              \inferrule*[Right=\tiny$\eqI$]{ }{y:B,x:A \cb (f(x)=y) \types (g(x)=g(x))}
            }{y:B,x:A \cb (f(x)=y) \types (f(x)=y) \meet (g(x)=g(x))
            }}{y:B,x:A \cb (f(x)=y) \types \exists x:A.((f(x)=y) \meet (g(x)=g(x)))
          }}{y:B,x:A \cb (f(x)=y) \types \exists z:C.\exists x:A.((f(x)=y) \meet (g(x)=z))
        }}{y:B \cb\ec \types \exists z:C.\exists x:A.((f(x)=y) \meet (g(x)=z))}
      \]
      \caption{Derivation tree of~\ref{item:eere1} in proof of \cref{thm:logic-extepi-regepi}}
      \label{fig:eere1}
    \end{figure}

    A corresponding derivation tree is shown (with some parts abbreviated) in \cref{fig:eere1}.
    The derivation trees of the next two would be even harder to fit on a page, but there is nothing tricky about translating the informal proofs into derivations.
    Thus we leave it to the reader, with some hints about which rules are being used.
  \item Suppose we have $y:B$ and $z_1,z_2:C$, and assume $\ph[z_1/z]$ and $\ph[z_2/z]$, that is to say $\exists x:A.(f(x)=y \meet g(x)=z_1)$ and $\exists x:A.(f(x)=y \meet g(x)=z_2)$.
    Let $x_1,x_2:A$ be such (using $\existsE$), so that $f(x_1)=y$ and $g(x_1)=z_1$, while $f(x_2)=y$ and $g(x_2)=z_2$.
    Then $f(x_1)=f(x_2)$ (using transitivity of equality), so by our other axiom, $g(x_1)=g(x_2)$; hence (using transitivity of equality again) $z_1=z_2$.
  \item Suppose we have $x:A$ and $y:B$ and $z:C$, and that $f(x)=y$ and $\ph$, i.e.\ $\exists x:A.(f(x)=y \meet g(x)=z)$.
    Let $x':A$ be such an element (using $\existsE$), so that $f(x')=y$ and $g(x')=z$.
    Then $f(x) = f(x')$ (by transitivity), so by our second axiom, $g(x) = g(x')$, and therefore (by transitivity) $g(x) = z$.\qedhere
  \end{enumerate}
\end{proof}

As always, this logical proof can be ``compiled out'' to a proof using commutative diagrams; see for instance~\cite[A1.3.4]{ptj:elephant}.
However, I find the logical proof much easier to understand.


\subsection{Coherent categories}
\label{sec:coherent-categories}

For coherent logic, there are few surprises.

\begin{defn}
  A \textbf{coherent category} is a regular category in which the posets $\sub(\Gamma)$ have finite unions that are preserved by pullback.
\end{defn}

\begin{thm}\label{thm:coherent-subobjects}
  A regular category \cS is coherent if and only if $\sub_\cS$ is a coherent hyperdoctrine.
\end{thm}
\begin{proof}
  If $\sub_\cS$ is a coherent hyperdoctrine, then clearly its joins are unions in the subobject posets of \cS, and the Beck--Chevalley condition implies these are stable under pullback.
  The converse is just as easy except for the presence of an additional context $\Theta$ in the rule for $\join$ (and similarly $\bot$, but we leave that case to the reader): we must show that if $\Theta \cap \ph \le \chi$ and $\Theta \cap \psi\le \chi$ in $\sub(\Gamma)$, then $\Theta \cap (\ph\cup \psi) \le \chi$.
  But $\Theta \cap \ph \le \chi$ in $\sub(\Gamma)$ is equivalent to $m^*\ph \le m^*\chi$ in $\sub(\Theta)$, where $m:\Theta\mono \Gamma$ is the given monomorphism, and similarly for the other conditions; so this also follows from pullback-stability of unions.
\end{proof}

In particular, in a coherent category, every object has a smallest subobject $0_A \mono A$.
It is not obvious, but true, that for any object $A$, the domain $0_A$ of this smallest subobject is an initial object (and hence isomorphic to $0_B$ for any other $B$).
For this purpose we need an additional lemma.

First note that although \crefrange{thm:logic-extremal-epi}{thm:logic-uniquechoice-funct} in \cref{sec:regular-categories} were stated for regular theories, they are in fact valid for theories in any fragment of logic \emph{containing} regular logic, and for any category \cS such that $\sub_\cS$ interprets that fragment of logic.
In particular, they are valid for coherent theories and coherent categories.
Second, we need the following further enhancement of \cref{thm:logic-uniquechoice}, whose proof we leave to the reader (\cref{ex:logic-uniquechoice-2}).

\begin{lem}\label{thm:logic-uniquechoice-2}
  Suppose we have a theory in a logic containing regular logic containing two types $A,B$ and propositions
  \begin{mathpar}
    x:A\types \alpha\prop\and
    y:B\types \beta\prop\and
    x:A,y:B\types \ph\prop
  \end{mathpar}
  such that the following sequents are provable:
  \begin{mathpar}
    x:A,y:B\cb\ph \types \alpha\and
    x:A,y:B\cb\ph \types \beta\and
    x:A \cb \alpha \types \exists y:B.(\beta\meet\ph)\and
    x:A,y_1:B,y_2:B \cb \alpha, \beta[y_1/y], \beta[y_2/y], \ph[y_1/y], \ph[y_2/y] \types y_1=y_2
  \end{mathpar}
  Then for any interpretation of this theory in a category \cS such that $\sub_\cS$ models the appropriate logic, the interpretation of $\ph$ yields (as in \cref{thm:logic-uniquechoice}) a morphism from the interpretation of $\alpha$ to the interpretation of $\beta$.\qed
\end{lem}

\begin{thm}
  If $0_A \mono A$ is the smallest subobject of $A$ in a coherent category, then $0_A$ is an initial object.
\end{thm}
\begin{proof}
  Let $B$ be any other object, and consider the coherent theory with two types $A$ and $B$ and nothing else.
  In this theory, let $\alpha = \bot$, $\beta=\top$, and $\ph=\bot$.
  Then all the sequents \cref{thm:logic-uniquechoice-2} have a $\bot$ in their proposition context, hence follow immediately from $\bot E$.
  Since $0_A$ is the interpretation of $\alpha$ and $B$ is the interpretation of $\beta$, we get a morphism $0_A \to B$.

  To show that it is unique, consider the theory with two objects $Z$ and $B$ and two morphisms $f,g:Z\to B$, and the axiom $z:Z \cb \ec \types \bot$.
  This is modeled by any two parallel morphisms in a coherent category whose domain has exactly one subobject (up to isomorphism), which is the case whenever its domain is the smallest subobject of some other object (like $0_A$).
  In this theory, we can prove $z:Z \cb \ec \types f(z) = g(z)$ by $\bot E$, which easily implies $f=g$.
\end{proof}

We leave some further basic facts about coherent categories to the reader as \cref{ex:coherent-strictinitial,ex:coherent-effunions}.


\subsection{Heyting categories}
\label{sec:heyting-categories}

Finally, we add the rest of the structure of first-order logic: universal quantification and implication.

\begin{defn}
  A \textbf{Heyting category} is a coherent category \cS such that for every $f:\Gamma\to\Delta$ in \cS, the pullback functor $f^*: \sub(\Delta) \to\sub(\Gamma)$ has a right adjoint.
\end{defn}

\begin{thm}\label{thm:heyting-subobjects}
  A coherent category \cS is a Heyting category if and only if $\sub_\cS$ is a first-order hyperdoctrine.
\end{thm}
\begin{proof}
  Since \cS is assumed to be coherent and in particular regular, by \cref{ex:reg-allbc} the \emph{left} adjoints of $f^*$ satisfy the Beck--Chevalley condition for pullbacks of projections.
  Thus, by \cref{ex:beck-chev}, if these functors also have right adjoints, they automatically satisfy the Beck--Chevalley condition for all pullback squares as well, and in particular for pullbacks of projections.
  Thus, if \cS is Heyting, then $\sub_\cS$ has universal quantifiers.
  For implication, we note that the Heyting exponential $A\to B$ in $\sub(\Gamma)$ can equivalently be constructed by first pulling back from $\sub(\Gamma)$ to $\sub(A)$, then applying the right adjoint to this pullback; this operation is stable under pullback by the same Beck--Chevalley condition.

  Conversely, suppose $\sub_\cS$ is a first-order hyperdoctrine, and in particular has universal quantifiers.
  We consider two first-order theories, both with two types $A,B$, a morphism $f:A\to B$, and atomic propositions $x:A \types P(x)\prop$ and $y:B \types Q(y)\prop$.
  \begin{enumerate}
  \item Our first theory adds to this the axiom $x:A \cb Q(f(x))\types P(x)$.
    We will show from this that $y:B \cb Q(y) \types (\forall x:A. (f(x)=y) \To P(x))$.
    By the rules for $\all$ and $\To$, it suffices to derive $x:A,y:B \cb Q(y), (f(x)=y)\types P(x)$.
    But then applying the rule for equality, it suffices to derive $x:A \cb Q(f(x)) \types P(x)$, which was an axiom.
  \item Our second theory instead takes $y:B \cb Q(y) \types \types (\forall x:A. (f(x)=y) \To P(x))$ as an axiom.
    Applying the rules for $\all$ and $\To$ in the other direction, we get $x:A,y:B \cb Q(y), (f(x)=y) \types P(x)$.
    Substituting $f(x)$ for $y$ in this, we get $x:A\cb Q(f(x)), (f(x)=f(x)) \types P(x)$; but since $f(x)=f(x)$ is true by reflexivity we can cut to get $x:A \cb Q(f(x))\types P(x)$.
  \end{enumerate}
  Thus, if we define $\all f(P)$ by $y:B \types (\forall x:A. (f(x)=y) \To P(x))\prop$, we see that it has the correct universal property to be a right adjoint of pullback $f^*$ (the latter given by substitution of $f(x)$ for $y$).
\end{proof}

Heyting categories are thus in some sense the most natural categorical home for first-order logic.
One origin of Heyting categories is explored in \cref{ex:lccc,ex:presheaves-sheaves}: any locally cartesian closed category with finite colimits is a Heyting category, including all elementary toposes and quasitoposes (which, as we will see in \cref{chap:hol}, also model \emph{higher}-order logic).
This book is not about the category theory of (quasi)toposes, but we encourage the reader to learn more about them; some good sources are~\cite{mm:shv-gl,mclarty:ecat-etop,ptj:elephant,wyler:quasitopoi}.
In particular~\cite{ptj:elephant} includes a comprehensive discussion of regular, coherent, and Heyting categories from a purely category-theoretic viewpoint.


\subsection*{Exercises}

\begin{ex}\label{ex:fptheory-horn}
  Suppose given a finite-product theory in the sense of \cref{sec:fp-theories}.
  Then we can make it into a Horn theory by replacing its $\equiv$ axioms with $=$ axioms (with empty proposition context).
  If \cS is any category with finite limits, prove that models of the original finite-product theory in \cS correspond bijectively to models of the Horn theory in $\sub_\cS$.
  In this sense, first-order logic subsumes finite-product logic; see \cref{ex:sieves} for a further enhancement.
\end{ex}

\begin{ex}\label{ex:regular-epis}
  Prove that every regular epimorphism (in any category) is an extremal epimorphism.
\end{ex}

\begin{ex}\label{ex:regular-egs}
  Prove that if \cS is a regular category and \cT is any finite-product theory (see \cref{sec:fp-theories}), then the category of \cT-models in \cS is also regular.
\end{ex}

\begin{ex}\label{ex:regular-not-coherent}
  Give an example of a regular category that is not a coherent category.
\end{ex}

\begin{ex}\label{ex:factsys}
  A (\textbf{unique} or \textbf{orthogonal}) \textbf{factorization system} on a category \cS is a pair $(\cE,\cM)$ of classes of morphisms in \cS such that
  \begin{enumerate}
  \item \cE and \cM are both closed under composition with isomorphisms;
  \item every morphism $f$ in \cS factors as $f=m e$ where $m\in\cM$ and $e\in\cE$; and
  \item if $m h = k e$ with $m\in\cM$ and $e\in \cE$, there exists a unique $\ell$ such that $m\ell=k$ and $\ell e = h$ (as in \cref{thm:extremal-epi}\ref{item:ee2}).
  \end{enumerate}
  A factorization system is \textbf{stable} if \cE is stable under pullback (\cM is automatically so), and \textbf{proper} if every morphism in \cE is an epimorphism and every morphism in \cM is a monomorphism.
  \begin{enumerate}
  \item Prove that if $(\cE,\cM)$ is a proper, stable, factorization system on a category \cS with finite limits, there is a regular hyperdoctrine $\sub_\cM$ where $\sub_\cM(\Gamma)$ is the sub-poset of $\sub_\cS(\Gamma)$ consisting only of monomorphisms in \cM.
  \item If \cS additionally has finite coproducts that are stable under pullback, prove that $\sub_\cM(\Gamma)$ is a coherent hyperdoctrine.
  \item Show that both of the previous parts apply when \cS is the category of topological spaces and \cM consists of the subspace inclusions.
  \item Is there an analogue of \cref{thm:logic-uniquechoice} for $\sub_\cM$?
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:sieves}
  For any category \cS with finite products, define an \cS-indexed poset $\sieve_\cS$ by letting $\sieve_\cS(\Gamma)$ be the poset of sieves on $\Gamma$.
  (A \textbf{sieve} on an object $\Gamma$ is a sub-functor of the representable functor $\cS(-,\Gamma)$.
  More concretely, it is a set of morphisms with codomain $\Gamma$, closed under precomposition with arbitrary morphisms of \cS.)
  \begin{enumerate}
  \item Prove that $\sieve_\cS$ is always a first-order hyperdoctrine.
  \item If we make a finite-product theory into a Horn theory as in \cref{ex:fptheory-horn}, prove that models of the finite-product theory in \cS correspond bijectively to models of the Horn theory in $\sieve_\cS$.
    Thus, first-order logic subsumes finite-product logic even for categories having only finite products.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:reg-allbc}
  Prove that in a regular category, the pullback functor $f^*: \sub(\Delta) \to \sub(\Gamma)$ has a left adjoint for \emph{every} morphism $f:\Gamma\to\Delta$, and that these left adjoints satisfy the Beck--Chevalley condition with respect to every pullback square in \cS.
\end{ex}

\begin{ex}\label{ex:logic-uniquechoice-funct}
  Prove \cref{thm:logic-uniquechoice-funct}.
\end{ex}

\begin{ex}\label{ex:logic-extepi-regepi}
  Write out derivation trees for statements~\ref{item:eere2} and~\ref{item:eere3} in the proof of \cref{thm:logic-extepi-regepi}.
  Feel free to use transitivity of equality as a (derivable) rule, rather than writing it out explicitly in terms of $\eqR$.
\end{ex}

\begin{ex}\label{ex:regular-subobjects}
  Rewrite the proof of the ``if'' direction of \cref{thm:regular-subobjects} using regular logic rather than category theory.
\end{ex}

\begin{ex}\label{ex:logic-uniquechoice-2}
  Prove \cref{thm:logic-uniquechoice-2}.
\end{ex}

\begin{ex}\label{ex:coherent-strictinitial}
  Prove using coherent logic that in a coherent category, any morphism whose codomain is initial is an isomorphism.
\end{ex}

\begin{ex}\label{ex:coherent-effunions}
  Prove using coherent logic that if we have monomorphisms $A \mono C$ and $B\mono C$ in a coherent category, then the square
  \[ \xymatrix{ A\cap B \ar[r] \ar[d] & B \ar[d] \\ A \ar[r] & A\cup B} \]
  is a pushout as well as a pullback.
  Conclude that if two objects of a coherent category can be embedded as disjoint subobjects of some third object, then they have a coproduct.
  (A coherent category in which this is true for any two objects is called \emph{positive} or \emph{extensive}.)
\end{ex}

\begin{ex}\label{ex:unions-not-images}
  Let \cD be a distributive lattice that is not a complete lattice, and let \cS be its free coproduct completion; the elements of \cS are set-indexed families $\{a_i\}_{i\in I}$ of elements of \cD, and the morphisms $\{a_i\}_{i\in I}\to \{b_j\}_{j\in J}$ are functions $f:I\to J$ such that $a_i\le b_{f(i)}$ for all $i$.
  Prove that $\sub_\cS$ has the structure to model the type operations $\meet,\top,\join,\bot$, but not $\exis$.
\end{ex}

\begin{ex}\label{ex:coherent-not-heyting}
  Give an example of a coherent category that is not a Heyting category.
\end{ex}

\begin{ex}\label{ex:lccc}
  Suppose \cS is a category with finite limits.
  Prove:
  \begin{enumerate}
  \item If \cS has coequalizers that are stable under pullback, then it is a regular category.
  \item If \cS has all finite colimits that are stable under pullback, then it is a coherent category.
  \item If \cS has all finite colimits and is locally cartesian closed, then it is a Heyting category.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:presheaves-sheaves}\ 
  \begin{enumerate}
  \item Show that the category of presheaves on any small category has finite limits and colimits and is locally cartesian closed, hence is a Heyting category.\label{item:pshsh1}
  \item Show that if \cS is locally cartesian closed with finite colimits, and $\cT$ is a reflective subcategory of \cS whose reflector preserves finite limits, then \cT is also locally cartesian closed with finite colimits.\label{item:pshsh2}
  \end{enumerate}
  The categories obtained by applying~\ref{item:pshsh2} to~\ref{item:pshsh1} are called \textbf{Grothendieck topoi}.
\end{ex}


\begin{wip}
\section{Comprehension}
\label{sec:comprehension}

In \cref{thm:fol-initial} we showed that the syntax of first-order logic presents free hyperdoctrines, and in \cref{sec:subobjects} that certain kinds of categories give rise to hyperdoctrines of subobjects.
This is sufficient to enable us to interpret first-order logic into these kinds of categories.

However, for some purposes one would like to be able to present a free \emph{category} using logic (e.g.\ the free coherent category generated by a coherent theory), rather than just a free hyperdoctrine.
This is analogous to how the syntax of a finite-product theory directly presents a free cartesian multicategory, but for some purposes we would actually like it to generate a free category with products.
(Hyperdoctrines can be thought of as a sort of ``multicategory-like'' version of a category with well-behaved subobjects.)

In the case of finite-product theories, we had two solutions to this problem: we could include a product type operation in the type theory, or we could consider the category of contexts of the type theory rather than the multicategory of types.
Let us consider first an analogy of the latter construction.
The most directly analogous thing would be to start with a cartesian multicategory \bS and a presheaf \cP on \bS valued in the category of cartesian multiposets, as considered briefly at the beginning of \cref{sec:hyperdoctrines}.
We would then build a category whose objects compare to the most general sort of ``context'' that appears first-order logic: pairs $(\Gamma\cb\Theta)$, where $\Gamma$ is a list of objects of \cS and $\Theta$ is a list of objects of $\cP(\Gamma)$.

However, we will simplify this in a couple of ways.
Firstly, we continue to consider instead ordinary presheaves on categories \cS with finite products.
Secondly, as we saw in \cref{sec:horn-subobjects}, if a category has an indexed poset of subobjects then the latter is automatically a Horn hyperdoctrine, and in particular has finite meets.
Thus, we can similarly replace $\Theta$ by a single object of $\cP(A)$.

In the end, therefore, we will start with a category \cS with products and a \cS-indexed poset \cP that is at least a Horn hyperdoctrine, and construct a category whose objects are pairs $(A\cb\alpha)$ where $A$ is an object of \cS and $\alpha$ is an object of $\cP(A)$.
But what should the morphisms be?
A first guess might be that a morphism from $(A\cb\alpha)$ to $(B\cb\beta)$ would be a morphism $f:A\to B$ such that $\alpha \le f^*\beta$.
However, this would not give enough morphisms.

In particular, by \cref{thm:logic-uniquechoice} we know that if \cP is a regular hyperdoctrine, then any proposition $\ph$ satisfying certain conditions gives rise to a morphism in any regular category that \cP maps into.
But our guess in the previous paragraph would not produce such a morphism in general, so it cannot produce a regular category that \cP maps into.

The solution is to take \cref{thm:logic-uniquechoice}, or more precisely \cref{thm:logic-uniquechoice-2}, as a \emph{definition} of the morphisms.
That is, we \emph{define} a morphism from $(A\cb\alpha)$ to $(B\cb\beta)$ to be an object $\ph\in \cP(A\times B)$ such that the sequents in \cref{thm:logic-uniquechoice-2} are valid in \cP.
More precisely, we define a morphism to be a model in \cP of the regular theory that has two types $A,B$, three atomic propositions $\alpha,\beta,\ph$ in contexts $A$ and $B$ and $(A,B)$ respectively, and four axioms
\begin{mathpar}
  x:A,y:B\cb\ph(x,y) \types \alpha(x)\and
  x:A,y:B\cb\ph(x,y) \types \beta(y)\and
  x:A \cb \alpha(x) \types \exists y:B.\ph(x,y)\and
  x:A,y_1:B,y_2:B \cb \ph(x,y_1), \ph(x,y_2) \types (y_1=y_2)
\end{mathpar}
We will call this the \textbf{theory of maps}.
This definition can, of course, be reinterpreted in terms of the categorical structure of \cP, but we will have no need to do that.

Note that this definition only makes sense if \cP is at least a \emph{regular} hyperdoctrine, with existential quantifiers.
We will come back to this point in \cref{sec:lex-theories}; for the moment, we simply assume that \cP is at least regular.

\begin{thm}\label{thm:hdmap-cat}
  If \cP is a regular hyperdoctrine, then the above definition yields a category $\nMap(\cP)$.
\end{thm}
\begin{proof}
  TODO: Formulate in terms of co-categories.

  We define the composite of $\ph:(A\cb\alpha)\to (B\cb\beta)$ and $\psi:(B\cb\beta) \to (C\cb \gamma)$ to be
  \[ x:A,z:C \types (\exists y:B. (\ph(x,y) \meet \psi(y,z))) \prop \]
  We show that this defines another morphism by the following informal arguments, translated into formal regular logic.
  For instance, here are the proofs that the composite satisfies the axioms to be a morphism from $(A\cb \alpha)$ to $(C\cb\gamma)$.
  \begin{itemize}
  \item If $\exists y:B. (\ph(x,y) \meet \psi(y,z))$, then we have a $y:B$ such that $\ph(x,y)$, and so (since $\ph$ satisfies the axioms) $\alpha(x)$.
  \item Similarly, if $\exists y:B. (\ph(x,y) \meet \psi(y,z))$, then we have a $y:B$ such that $\psi(y,z)$, and so (since $\psi$ satisfies the axioms) $\gamma(z)$.
  \item If $\alpha(x)$, then since $\ph$ satisfies the axioms, there exists (and so we may assume we have) a $y:B$ such that $\ph(x,y)$.
    Moreover, since $\ph(x,y)$, we have $\beta(y)$.
    Now since $\psi$ also satisfies the axioms, there exists (and so we may assume we have) a $z:C$ such that $\psi(y,z)$.
    Using $y$, we conclude $\exists y:B.(\ph(x,y) \meet \psi(y,z))$, and therefore $\exists z:C.\exists y:B.(\ph(x,y) \meet \psi(y,z))$.
  \item Suppose we have $x:A$ and $z_1:C$ and $z_2:C$ such that $\exists y:B.(\ph(x,y) \meet \psi(y,z_1))$ and $\exists y:B.(\ph(x,y) \meet \psi(y,z_2))$.
    By using these latter two hypotheses, we may assume we have $y_1:B$ and $y_2:B$ such that $\ph(x,y_1)$ and $\psi(y_1,z_1)$, and also $\ph(x,y_2)$ and $\psi(y_2,z_2)$.
    Now since $\ph$ satisfies the axioms, we have $y_1=y_2$.
    Using this equality, we can change our assumption of $\psi(y_2,z_2)$ to $\psi(y_1,z_2)$.
    Therefore, since also $\psi(y_1,z_2)$ and $\psi$ satisfies the axioms, we have $z_1=z_2$.
  \end{itemize}
  More formally, what we are doing is considering a theory with three objects $A,B,C$, five atomic propositions $\alpha,\beta,\gamma,\ph,\psi$, and the axioms making $\ph$ and $\psi$ both morphisms of $\nMap(\cP)$.
  This could be described as the pushout, in the category of theories, of two copies of the theory of maps over the \emph{theory of objects} (which has one object $A$ and one atomic proposition $x:A \types \alpha(x)\prop$).
  We have just shown that the free hyperdoctrine generated by this theory contains \emph{another} model of the theory of maps.
  Therefore, by the universal property of free hyperdoctrines, any composable morphisms of $\nMap(\cP)$ give rise to a third one, which we define to be their composite.

  Similarly, we define the identity morphism of $(A\cb\alpha)$ is $x:A,y:A \types (\alpha(x) \meet (x=y))\prop$.
  Proving that this is a morphism gives a morphism from the theory of maps to the free hyperdoctrine generated by the theory of objects.
  We can similarly prove that composition is associative and unital; we leave the details to the reader (\cref{ex:hdmap-cat}).
\end{proof}

To show that $\nMap(\cP)$ has products, we need the following logical characterization of products.

\begin{lem}
  Consider the Horn theory with two objects $A$, $B$, and $P$, three morphisms $\pi_1:P\to A$, $\pi_2:P\to B$, and $p:(A,B) \to P$, and axioms
  \begin{mathpar}
    x:A,y:B \cb\ec\types \pi_1(p(x,y))=x\and
    x:A,y:B \cb\ec\types \pi_2(p(x,y))=y\and
    z:P \cb\ec\types p(\pi_1(z),\pi_2(z))=z
  \end{mathpar}
  For any category \cS with finite limits, a model of this theory in $\sub_\cS$ is precisely a binary product diagram.
\end{lem}
\begin{proof}
  Under interpretation in \cS, $p$ becomes a morphism $A\times B\to P$, while $\pi_1$ and $\pi_2$ pair up to yield a morphism $P\to A\times B$.
  The axioms ensure that the composites of these morphisms in both directions are the identity.
  (Note that this theory is obtained from a finite-product theory as in \cref{ex:fptheory-horn}; also compare to \cref{thm:cart-multicat-repr}.)
\end{proof}

Similarly, we have:

\begin{lem}
  Consider the Horn theory with one object $T$, one morphism $t:() \to T$, and one axiom
  \begin{mathpar}
    x:T \cb\ec\types x=t
  \end{mathpar}
  Then for any category \cS with finite limits, a model of this theory in $\sub_\cS$ is precisely a terminal object of \cS.\qed
\end{lem}

\begin{thm}\label{thm:hdmap-lex}
  If \cP is a regular hyperdoctrine, then $\nMap(\cP)$ (as defined in \cref{thm:hdmap-cat}) has finite limits.
\end{thm}
\begin{proof}
  [TODO]
  The product of $(A\cb\alpha)$ and $(B\cb\beta)$ is $(A\times B\cb \alpha\times\beta)$, where ``$\alpha\times\beta$'' denotes the proposition
  \[ z:A\times B \types (\alpha(\pi_1(z))\meet \beta(\pi_2(z)))\prop \]
  The terminal object is $(\unit\cb \top)$.
\end{proof}


% TODO: Where to put this?
% \begin{rmk}\label{rmk:subset-quotient}
%   Would introduce type dependency.
% \end{rmk}

\subsection*{Exercises}

\begin{ex}\label{ex:hdmap-cat}
  Fill in the details of \cref{thm:hdmap-cat}.
\end{ex}

\end{wip}


\section{Finite-limit theories}
\label{sec:lex-theories}

% Use a "cartesian proposition" judgment and the Yoneda embedding; though that only gives us interpretability and not initiality.
% Alternatively, if we have sequent calculus for a subformula property, we can show syntactically that derivations of entailments between cartesian formulae only use cartesian formulae, and thereby build a free "lex hyperdoctrine".

% Other things to try would introduce type dependency; maybe do some of them as a baby starting point in \cref{chap:dtt}.


\section{Indexed monoidal categories}
\label{sec:indexed-moncat}


\ChapterExercises

% Local Variables:
% TeX-master: "catlog"
% End: