With duals for objects
With duals for morphisms
Special sorts of products
In higher category theory
A locally cartesian closed category is a category whose slice categories are all cartesian closed.
If a locally cartesian closed category has a terminal object, then is itself cartesian closed and in fact has all finite limits (because, cartesian products in are pullbacks in ); often this requirement is included in the definition.
Equivalently, a locally cartesian category is a category with pullbacks (and a terminal object, if required) such that each base change functor has a right adjoint , 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.
Cartesian closure in terms of base change and dependent product
We show how the dependent product and the internal hom in the slice categories may be used to express each other.
In category theory
Let be a category with pullbacks that has all dependent products , equivalently that every morphism in induces an adjoint triple
Then the internal hom in a slice exists and is given by
By the discusson at overcategory-Limits and colimits the product in the slice of two objects and is given by the pullback in , regarded again as a morphism over . More formally this means that the product with is given by the composite
of the pullback along with the dependent sum along . 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 , the inner hom is explicitly given by
If for a category every slice category is a cartesian closed category, then for every morphism in the dependent product exists and is given on an object by the pullback
in , where the bottom morphism is the adjunct of
It is sufficient to check the -adjunction hom set-natural isomorphism
natural in .
Since the hom functor preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback
in Set. Using the -adjunction this is equivalently
This pullback now manifestly computes .
If is locally cartesian closed (i.e., if every slice is cartesian closed), then every slice is also locally cartesian closed.
The slice of a slice is a slice, i.e., for every there is an equivalence
whence the statement immediately follows.
If is locally cartesian closed (and has a terminal object), then the pullback functor preserves both finite products and exponentials up to isomorphism.
Clearly , being right adjoint to the forgetful functor , preserves limits, hence it preserves finite products in particular.
Let be any morphism. From the pullback diagram
we conclude , seen as an object over via . Thus arrows in the slice of the form
are in natural bijection with arrows in of the form
which in turn are in natural bijection with arrows in the slice of the form
(where is obtained by currying in ). This proves that preserves exponentials.
For any in , the base change preserves exponentials. In other words, the dependent sum functor and the dependent product functor satisfy Frobenius reciprocity.
This is by combining proposition 3 and proposition 4, and recalling that the pullback functor
is identified with the pullback functor .
This state of affairs may be summarized in terms of the notion of hyperdoctrine:
For a proof of the statement in this form, see for instance (Freyd).
In type theory
We formulate some of the above considerations in the syntax of dependent type theory.
be two display maps. Then the category theoretic identification
from prop. 1 is the categorical semantics of the dependent type theory syntax
By definition, the display map on the right is expressed as the dependent type
the pullback is expressed by substitution
and next the dependent product by
Now on the right , formally because is equivalently the projection out of 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 , and hence by definition this is the dependent function type
which expresses the internal hom in the slice over .
The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product represents an extensional dependent product type in the internal logic.
Almost local cartesian closure
There are categories which are cartesian closed and not locally cartesian closed, but in which for some the base change functor has a right adjoint. This includes , , and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for to be a fibration, while in it is sufficient for to be a fibration or an opfibration.
Every sheaf topos is locally cartesian closed.
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
- Peter Freyd, Aspects of topoi, Bull. Australian Math. Soc. 7 (1972), 1-76.
A discussion of dependent type theory as the internal language of locally cartesian closed categories is in
- R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)
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.