Internal category theory
Given a finitely complete category , one can consider the bicategory of internal categories in , and thus internal functors, which are the morphisms in . If then one can consider not only functors among small categories but also functors of the type from a small category to a large category of sets. In that case one can describe as consisting of a -indexed family of objects and an action of on the diagram.
Compare the ideas discussed on this page with those at internal profunctor and discrete fibration. All three notions intersect — an internal diagram on is the same thing as an internal profunctor , which is the same thing as a discrete opfibration in . The three generalize the basic idea in different ways.
In category theory
Given an internal category , with the usual structure maps , an internal diagram on (or, of type ) is given by
- a morphism in together with
- a morphism
where is the pullback
These data must satisfy the following conditions:
respects the source and target maps of , in that . Equivalently, is a morphism from to in .
is an action in the sense that and .
It is clear how to define homomorphisms of internal diagrams: a morphism is given by an -morphism that commutes with the actions . Internal diagrams on in form a category denoted by .
An internal diagram on is sometimes called an internal presheaf on .
In dependent type theory
Using the language of dependent types, the map can be seen as the interpretation of a dependent type . The action of on can equivalently be given by the interpretation of a term in context:
Here we consider to depend on by the canonical morphism induced by and , as in the type-theoretic definition of category.
If the ambient category is a locally cartesian closed category, so that its internal type theory has dependent product types, then this can be interpreted instead as a closed term
The axioms then take a particularly familiar form, also to be interpreted in the internal language of :
From an internal diagram one can equip with a structure of an internal category over . In other words, there is a forgetful functor (where is the corresponding slice category). This functor is fully faithful and its essential image consists precisely of all objects in which are discrete opfibrations. Similarly, the objects of are the discrete fibrations in .
There is a composite forgetful functor . This functor is monadic — its left adjoint takes to .
Diagrams in an indexed category
An internal diagram as above may take values in any Grothendieck fibration over . Given a fibration in the guise of an indexed category , a -diagram in is given by
- an object , together with
- a morphism in
satisfying ‘cocycle equations’
modulo coherent isos, where the are the projections out of .
By the Yoneda lemma for bicategories, the object determines (up to canonical isomorphism) a pseudonatural in , where is considered as a locally discrete bicategory, and considered as a discrete category, such that . Similarly, determines , and . It is not hard to check that the conditions above correspond to requiring that the form a functor for each , and pseudonaturality then makes the -diagram equivalent to an indexed functor . The category of -diagrams in is then simply the hom-category .
An internal diagram on in the sense above is a -diagram in the codomain fibration of , that is the pseudofunctor .
If is equipped with a coverage and is the Cech nerve associated to a cover in , then the category of -diagrams in is the descent category .