category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
A locally cartesian closed category is a category $C$ whose slice categories $C/x$ are all cartesian closed.
If a locally cartesian closed category $C$ has a terminal object, then $C$ is itself cartesian closed and in fact has all finite limits (because, cartesian products in $C/x$ are pullbacks in $C$); often this requirement is included in the definition.
Equivalently, a locally cartesian category $C$ is a category with pullbacks (and a terminal object, if required) such that each base change functor $f^*: C/y \to C/x$ has a right adjoint $\Pi_f$, called the dependent product. (This equivalence is discussed in detail below.)
In particular, such pullbacks preserve all colimits. Therefore, if a locally cartesian closed category has finite colimits, it is automatically a coherent category and in fact a Heyting category.
We show how the dependent product and the internal hom in the slice categories may be used to express each other.
Let $\mathcal{C}$ be a category with pullbacks that has all dependent products $\prod_\bullet$, equivalently that every morphism $f : E \to X$ in $\mathcal{C}$ induces an adjoint triple
Then the internal hom in a slice $\mathcal{C}_{/X}$ exists and is given by
By the discusson at overcategory-Limits and colimits the product in the slice $\mathcal{C}_{/X}$ of two objects $\langle E_1 \stackrel{f_1}{\to} X\rangle$ and $\langle E_1 \stackrel{f_2}{\to} X\rangle$ is given by the pullback $f_1^* E_2 = f_2^* E_1$ in $\mathcal{C}$, regarded again as a morphism over $X$. More formally this means that the product with $\langle E \stackrel{f}{\to} X\rangle$ is given by the composite
of the pullback along $f$ with the dependent sum along $f$. By the above adjoint triple both these morphisms have right adjoints and so the composite of the right adjoints is the right adjoint of the composite, hence is the internal hom:
In the slice category $Set/X$, the inner hom is explicitly given by
If for a category $\mathcal{C}$ every slice category is a cartesian closed category, then for every morphism $f : X \to Y$ in $\mathcal{C}$ the dependent product $\prod_f$ exists and is given on an object $E \stackrel{p}{\to} X$ by the pullback
in $\mathcal{C}_{/Y}$, where the bottom morphism is the adjunct of
It is sufficient to check the $(f^* \dashv \prod_f)$-adjunction hom set-natural isomorphism
natural in $\langle F \stackrel{}{\to}Y \rangle$.
Since the hom functor $\mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, -)$ preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback
in Set. Using the $((-) \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to}Y\rangle \dashv [\langle X \stackrel{f}{\to}Y\rangle, -]_{\mathcal{C}_{/Y}})$-adjunction this is equivalently
This pullback now manifestly computes $\mathcal{C}_{/X}(f^* \langle F \to Y\rangle, \langle E \stackrel{p}{\to} X\rangle)$.
If $C$ is locally cartesian closed (i.e., if every slice $C/X$ is cartesian closed), then every slice $C/X$ is also locally cartesian closed.
The slice of a slice is a slice, i.e., for every $f \colon X \to Y$ there is an equivalence
whence the statement immediately follows.
If $C$ is locally cartesian closed (and has a terminal object), then the pullback functor $X \times - \colon C \to C/X$ preserves both finite products and exponentials up to isomorphism.
Clearly $X \times - \colon C \to C/x$, being right adjoint to the forgetful functor $\sum_X \colon C/X \to C$, preserves limits, hence it preserves finite products in particular.
Let $\phi \colon A \to X$ be any morphism. From the pullback diagram
we conclude $A \times_X (X \times Z) \cong A \times Z$, seen as an object over $X$ via $\phi \circ \pi_A \colon A \times Z \to X$. Thus arrows in the slice $C/X$ of the form
are in natural bijection with arrows in $C$ of the form
which in turn are in natural bijection with arrows in the slice $C/X$ of the form
(where $\tilde{g} \colon A \to Y^Z$ is obtained by currying $g \colon A \times Z \to Y$ in $C$). This proves that $X \times - \colon C \to C/x$ preserves exponentials.
For any $f \colon X \to Y$ in $C$, the base change $f^\ast \colon C/Y \to C/X$ preserves exponentials. In other words, the dependent sum functor $\sum_f$ and the dependent product functor $\prod_f$ satisfy Frobenius reciprocity.
This is by combining proposition 3 and proposition 4, and recalling that the pullback functor
is identified with the pullback functor $f^\ast \colon C/Y \to C/X$.
This state of affairs may be summarized in terms of the notion of hyperdoctrine:
If $C$ is a category with finite limits, then it is locally cartesian closed precisely if regarded as an $C$-indexed category (by forming slice categories) it is a hyperdoctrine.
For a proof of the statement in this form, see for instance (Freyd).
We formulate some of the above considerations in the syntax of dependent type theory.
Let
be two display maps. Then the category theoretic identification
from prop. 1 is the categorical semantics of the dependent type theory syntax
While equivalent under the relation between type theory and category theory, the latter expression almost verbatim expresses the evident idea that:
(collection of internal homs parameterized over $B$) = ( collection of sections of the pullback of $A$ to $X$ )
By definition, the display map on the right is expressed as the dependent type
the pullback $f^* \langle A \to B\rangle$ is expressed by substitution
and next the dependent product $\prod_\phi \phi^* \langle A \to B\rangle$ by
Now on the right $\phi(x) =_{def} b$, formally because $\phi$ is equivalently the projection $pr_1$ out of $X$ expressed as the direct sum
Inserting this in the above expression makes it definitionally equal to
This in now a dependent product over a type that does not actually depend on the context $B$, and hence by definition this is the dependent function type
which expresses the internal hom in the slice over $B$.
The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product $\Pi_f$ represents an extensional dependent product type in the internal logic.
There are categories which are cartesian closed and not locally cartesian closed, but in which for some $f$ the base change functor $f^*: C/y \to C/x$ has a right adjoint. This includes $Cat$, $Gpd$, and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for $f$ to be a fibration, while in $Cat$ it is sufficient for $f$ to be a fibration or an opfibration.
Every sheaf topos is locally cartesian closed.
By Giraud's theorem, in a sheaf topos pullbacks preserve colimits. With the adjoint functor theorem this implies that for every morphism $f : X \to Y$, the pullback functor $f^* : \mathcal{C}_{/Y} \to \mathcal{C}_{/X}$ has a right adjoint $\prod_f$. By prop. 1 this yields the local cartesian closure.
cartesian closed category, locally cartesian closed category
cartesian closed model category, locally cartesian closed model category
cartesian closed (β,1)-category locally cartesian closed (β,1)-category
A standard textbook account is around corollary A1.5.3 in
The relation between local cartesian closure and base change/hyperdoctrine structure is sometimes attributed to
A discussion of dependent type theory as the internal language of locally cartesian closed categories is in
Related literature includes
Marta Bunge, and Susan Niefield, Exponentiability and single universes J. Pure Appl. Algebra 148 (2000) 217β250.
FranΓ§ois ConduchΓ©, Au sujet de lβexistence dβadjoints Γ droite aux foncteurs βimage rΓ©ciproqueβ dans la catΓ©gorie des catΓ©gories (French) C. R. Acad. Sci. Paris SΓ©r. A-B 275 (1972), A891βA894.
J. Howie, Pullback functors and crossed complexes , Cahiers Topologie GΓ©om. DiffΓ©rentielle, 20 (1979) 281β296.