We introduce the theory of enrichment over an internal monoidal category as a common generalization of both the standard theories of enriched and internal categories. Then, we contextualize the new notion by comparing it to another known generalization of enrichment: that of enrichment for indexed categories. It turns out that the two notions are closely related.
Notes
Communicated by Nicola Gambino.
Research funded by Cambridge Trust and EPSRC.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
Categories, even large ones, are said to be complete if they have limits for merely all small diagrams, and various size issues originate from this. Small categories avoid this pitfall, but, unfortunately, the only small complete categories are the complete preorders (a well-known, though unpublished, result by Freyd).
Internalizing the notion of small category yields that of internal category, which is thus well-behaved with respect to size. Moreover, the internal logic of realizability toposes allows for small complete categories that are not preorders, as Freyd’s degeneracy result relies on classical logic. For example, the category of modest sets in the effective topos (or, more precisely, in its subcategory of assemblies) is complete despite not being a preorder [7‐9].
Advertisement
Unfortunately, the theory of internal categories is not as expressive as we might like. For example, it’s generally not possible to formulate the notion of presheaf in the internal context, because internal categories do not come with an enriching category the way that locally small categories are enriched over \({{\,\mathrm{Set}\,}}\). To overcome these limitations, this paper presents and develops a theory of internal enrichment which combines the pleasantness of internal categories with respect to size issues with the expressivity of enriched categories.
The paper starts by recalling some background material. Section 2 briefly introduces the fundamental notions of internal category theory, by use of the internal language of the ambient category in an informal style.
Section 3 presents the notion of monoidal structure for internal categories and discusses the theory of internal monoidal categories, which will be used as the enriching categories for the proposed notion of internal enriched category.
Section 4 quickly recalls the notion of indexed category, together with some basic element of the theory of fibrations and their relation to indexed categories via the Grothendieck construction, with a focus on the case of indexed monoidal categories and monoidal fibrations.
Advertisement
Section 5 presents the construction of the externalization of an internal category, which yields an indexed category over the ambient category. We focus in particular on the externalization of internal monoidal categories, which yields indexed monoidal categories.
Section 6 introduces the theory of internal enrichment over an internal monoidal category, obtained by internalizing the standard theory of enrichment over a monoidal category. The section presents the definitions of internal enriched category, i.e., of an internal category enriched over an internal monoidal category, of functor between internal enriched category and of natural transformation between such functors. It discusses the 2-category of internal enriched categories, functors and natural transformations, and issues of change of base.
Finally, Sect. 7 places internal enrichment in the landscape of notions of generalized enrichment by showing that internal enriched categories are closely related to enriched indexed categories [15, 16] via externalization. This ties together the notion of internal enriched category with all of the background material presented in the early sections of the paper.
From an application perspective, we believe internal enrichment can be a valuable tool in the study of categorical models for polymorphism, in theoretical computer science. Indeed, Eugenio Moggi originally suggested that the effective topos contains a small complete subcategory as a way to understand how realizability toposes give rise to models for impredicative polymorphism, and concrete versions of such models first appeared in [5]. Moreover, [14] noted that set theory is inadequate to treat polymorphism, and [13] overcame the issue by internalizing the model in a suitable topos. Finally, [6] has presented a model for higher-order polymorphic lambda-calculus based on enrichment over the category of partial equivalence relations, and noticed that inconveniently this category is incomplete, although it is internally complete in the effective topos [8]. Thus, internal and enriched categories are essential tools in the treatment of polymorphism. Internal enriched categories, being their common generalization and carrying the benefits of both, would remove the necessity of picking one and allow for a natural extension of the known models.
This paper is based on the author’s doctoral research [3]. Further developments on the theory of internal enrichment, particularly in the direction of a theory of completeness, are already contained in the dissertation.
2 Internal Categories
In this section we quickly set some notation with regard to internal categories, without actually discussing their theory. Such notation is mostly standard, as it is fundamentally similar to that used in well-known textbooks [1, 11]. A brief account of the theory of internal categories adopting the notation of this section can be found in [4].
In the context of this paper, let be a category with finite limits, which we regard as our ambient category. To be precise, in particular we require to have a cartesian monoidal structure, that is, a monoidal structure given by a functorial choice of binary products and a chosen terminal object . As a category with finite limits, is a model for cartesian logic, or finite limit logic. We will frequently use the internal language of to ease the notation, although in an informal style. At the cost of readability, the given formulas could be elaborated either into the language of Freyd’s essentially algebraic theories [2], or into Johnstone’s cartesian logic [10], or into the partial Horn logic of Palmgren and Vickers [12], other than into commutative diagrams.
We start by giving the definition of internal category in .
Definition 1
(internal category) An internal category\(\mathbf {A}\) in is a diagram
in (where is the pullback of and ) satisfying the usual axioms for categories, which can be expressed in the internal language of by the formulae
where is the pullback of and , and is the iterated pullback. Notice that, by the universal property of the pullback, if and only if \(f :A_1\), \(g :A_1\), and , in the sense that local sections correspond bijectively to pairs of local sections \(f, g :X \rightarrow A_1\) such that .
×
We now define functors of internal categories. Then internal categories and their functors form a category .
Definition 2
(internal functor) Let \(\mathbf {A}\) and \(\mathbf {B}\) be internal categories in . A functor of internal categories \(F :\mathbf {A}\rightarrow \mathbf {B}\) is given by a pair of arrows \(F_0 :A_0 \rightarrow B_0\) and \(F_1 :A_1 \rightarrow B_1\) such that
The composition (shortened in GF for brevity) of two consecutive internal functors \(F :\mathbf {A}\rightarrow \mathbf {B}\) and \(G :\mathbf {B}\rightarrow \mathbf {C}\), and the identity functor for an internal category \(\mathbf {A}\), are defined in the usual way.
The following result is the internal version of the standard set-theoretic one, and it can be proved by a completely routine application of the internal language of .
Proposition 1
The category has finite limits induced point-wise by the corresponding limits in . In particular, there is a terminal internal category and a binary product of internal categories making a cartesian monoidal category.
Let be another category with finite limits, and a functor preserving finite limits. Then, there is a change-of-base functor applying F to the underlying graph of internal categories. In the following remark, we notice some useful properties of in relation to slicing and change of base.
Remark 1
Let \(i :J \rightarrow I\) be an arrow in . Then, there is an adjunction where the functor is given by post-composition with i, and the functor is given by pullback along i. This adjunction extends to internal categories, yielding . In particular, the unique arrow yields an adjunction .
Proposition 2
Let be a functor between categories with finite limits which preserves such finite limits. Then, the induced change-of-base functor preserves finite limits.
There is also an obvious objects functor sending an internal category to its underlying object-of-objects. This functor preserves the cartesian monoidal structure. We then mention a few remarkable examples of internal categories:
\({{\,\mathrm{dis}\,}}A\), the discrete category over an object A.
\({{\,\mathrm{ind}\,}}A\), the indiscrete category over an object A.
\(\mathbf {A}^{{{\,\mathrm{op}\,}}}\), The opposite category of an internal category \(\mathbf {A}\).
Then, we have the following adjunctions:
.
.
An alternative, more abstract way to look at the discrete category with respect to Remark 1 is to notice that \({{\,\mathrm{dis}\,}}A\) is (isomorphic to) .
We now define natural transformations of internal categories. Internal categories, together with their functors and the natural transformations between them, form a 2-category (denoted in the same way as its underlying 1-category with abuse of notation; context usually suffices to distinguish whether we are referring to the underlying 1-category or the 2-category).
Definition 3
(internal natural transformation) Let \(F, G :\mathbf {A}\rightarrow \mathbf {B}\) be functors of internal categories in . A natural transformation of internal functors \(\alpha :F \rightarrow G :\mathbf {A}\rightarrow \mathbf {B}\) is given by an arrow \(\alpha :A_0 \rightarrow B_1\) such that
Vertical and horizontal compositions of natural transformations and the identity natural transformation are defined in the usual way.
To clarify a subtlety of the notation, notice that denotes the identity of the category \(\mathbf {A}\), while denotes the identity functor on \(\mathbf {A}\) and denotes the identity natural transformation on \(F :\mathbf {A}\rightarrow \mathbf {B}\). When it is clear from the context, we might omit the subscript of and write, for example, in place of and in place of .
Sometimes, and especially when using the internal language, the notation denoting the object or morphism components of a functor can be cumbersome. Thus, in the following sections we shall adopt a common convention in category theory and omit to make such components explicit when it is clear from the context which one we are referring to. For example, given an internal functor \(F :\mathbf {A}\rightarrow \mathbf {B}\), in context \(a :A_0, f :A_1\) we shall write F(a) for \(F_0(a)\) and F(f) for \(F_1(f)\).
3 Internal Monoidal Categories
We could not conceivably present a notion of enrichment without a suitable notion of monoidal category to enrich over. We introduce here the definitions, in the internal language of , of the notions of monoidal category, functor and natural transformation.
Definition 4
(internal monoidal category) An internal monoidal category is an internal category \(\mathbf {V}\) in equipped with functors
Monoidal product: , and
Monoidal unit: ,
and natural isomorphisms
Associator: ,
Left unitor: , and
Right unitor: ,
such that, in context \(a, b, c, d :V_0\), the axioms
hold. Here, the diagrams are just convenient representations of formulae in the internal language of the ambient category . For example, Equation 1 represents the following formula.
Such translation is straightforward, but we favour the diagrammatic representation as it is more intuitive and familiar to the category theorist.
×
The previous definition is a direct internalization of the standard definition of monoidal category, and that alone should suffice to persuade us of its correctness. If we were still skeptical, though, it could also be argued that, since small monoidal categories are pseudomonoids in the 2-category of categories, then internal monoidal categories in must be pseudomonoids in the 2-category , which is what our definition amounts to.
We then proceed with the definition of monoidal functor.
Definition 5
(internal monoidal functor) An internal monoidal functor is given by an internal functor and coherence natural isomorphisms
and
such that, in context \(a, b, c :V_0\), the axioms
hold.
×
Then, we define natural trasformations of monoidal functors.
Definition 6
(internal monoidal natural transformation) An internal monoidal natural transformation is a natural transformation such that, in context \(a, b, :V_0\), the axioms
hold.
×
It is routine to check in the internal language that the data above gives 2-categories, so we can give the following definitions.
Definition 7
(category of internal monoidal categories) Internal monoidal categories and monoidal functors in form a category . Moreover, monoidal natural transformations in give the structure of a 2-category (denoted in the same way as its underlying 1-category with abuse of notation; context usually suffices to distinguish whether we are referring to the underlying 1-category or the 2-category).
As for internal categories (see Proposition 2), we can transport the monoidal structure along a functor changing the base category.
Proposition 3
Let be a functor between categories with finite limits which preserves such finite limits. Then, there is an induced change-of-base functor , which also preserves finite limits.
Finally, notice that there is an underlying-internal-category 2-functor
sending monoidal categories, functors and natural transformations to, respectively, their underlying internal categories, functors and natural transformations.
4 Indexed Categories
Indexed categories, while not playing a direct role in the definition of internal enrichment, will be essential to their understanding in relation to other notions of enrichment.
Indexed categories have been treated extensively in the literature, and the main ideas are long established. However, we shall refer to the recent exposition given in [15, 16], since these sources are also needed in regard to the notion of enriched indexed category.
To begin with, we state the definition of indexed category.
Definition 8
(indexed category) An -indexed category is a pseudofunctor , where is the 2-category of categories, functors, and natural transformations.
Consider the following notable example, which will turn out to be useful later on.
Example 1
The self-indexing of is the -indexed category whose fiber over an object X is the slice category and where the reindexing along \(f :X \rightarrow Y\) is given by pullback along f.
Next, we state the definition of fibration.
Definition 9
(fibration) An arrow \(l :A' \rightarrow A\) in \(\mathscr {F}\) is cartesian with respect to a functor if, for any other arrow \(h :A'' \rightarrow A\) in \(\mathscr {F}\) and \(g :P(A'') \rightarrow P(A')\) in such that \(P(l) g = P(h)\), there exists a unique \(k :A'' \rightarrow A'\) in \(\mathscr {F}\) such that \(l k = h\) and \(P(k) = g\).
A functor is a fibration if for any A in \(\mathscr {F}\) and \(f :X \rightarrow P(A)\) there is a cartesian arrow \(l :A' \rightarrow A\) such that \(P(l) = f\), called the cartesian lifting of f. Moreover, a fibration is cloven if it comes with a choice of cartesian liftings.
There is a strict relation between the theory of indexed categories and that of fibrations, as established by the following, classic result.
Theorem 1
An -indexed category is, via the Grothendieck construction, equivalent to a cloven fibration . More precisely, there is an equivalence of bicategories (and, in fact, an equivalence of strict 2-categories [10]), where is the 2-category of cloven fibrations over , strong morphisms of fibrations, and transformations of fibrations.
Now we want to extend the previous ideas to the context of monoidal categories. We begin by giving the notion of indexed monoidal categories.
Definition 10
(indexed monoidal category) An -indexed monoidal category is a pseudofunctor , where is the 2-category of monoidal categories, strong monoidal functors, and monoidal transformations.
A suitable notion of monoidal fibration is required to establish a relation with indexed monoidal categories, so we recall that in the following definition.
Definition 11
(monoidal fibration, Definition 12.1 [15]) Let \(\mathscr {V}\) be a monoidal category. A monoidal fibration is a cloven fibration such that the underlying functor is strict monoidal (with regarded as cartesian monoidal) and the tensor product in \(\mathscr {V}\) preserves cartesian arrows.
For a general monoidal base category the notions of indexed monoidal category and of monoidal fibration do not correspond under the Grothendieck construction. Indeed, if is an -indexed monoidal category, then, in the cloven fibration , it is evident that has tensor products only for objects in the same fiber, and the result is still an object in that fiber. On the other hand, if is a monoidal fibration, and A and B are objects of \(\mathscr {V}\) lying over the objects X and Y of respectively, then the tensor product lies over . However, in case the monoidal structure on is given by the product, i.e., is cartesian monoidal, such as our ambient category is, then there is a correspondence (for details, see Theorem 12.7 from [15]). We recall this result in the following theorem.
Theorem 2
An -indexed monoidal category is, via the Grothendieck construction, equivalent to a monoidal fibration . More precisely, there is an equivalence of bicategories , where is the 2-category of monoidal fibrations over , strong monoidal morphisms of fibrations, and monoidal transformations of fibrations.
5 Externalization of Internal Categories
The last piece of background material that we present concerns the relationship between internal and indexed categories, and makes an essential use of the theory of indexed categories from Sect. 4. For the central notion of externalization of an internal category, we shall follow the exposition of [8, 9].
Let \(\mathbf {A}\) be a category in and X an object of . We regard an arrow \(X \rightarrow A_0\) as representing an indexed family of objects of \(\mathbf {A}\) over the indexing object X. Given two such indexed families \(x_0, x_1 :X \rightarrow A_0\), consider the pullback
Then the sections of p represent indexed families of arrows of \(\mathbf {A}\) with domain \(x_0\) and codomain \(x_1\). Given another family \(x_2 :X \rightarrow A_0\), the composition in \(\mathbf {A}\) restricts to an indexed composition
inducing a composition of indexed families of arrows: given two families of arrows \(s_0 :X \rightarrow {(x_0, x_1)}^{*}A_1\) and \(s_1 :X \rightarrow {(x_1, x_2)}^{*}A_1\), their composition is defined as
Moreover, a family of objects \(x :X \rightarrow A_0\) induces a family of identity arrows . These data form the category of indexed families of objects and morphisms of \(\mathbf {A}\) over X.
×
Given a reindexing \(u :X' \rightarrow X\), precomposition reindexes a family of objects \(x :X \rightarrow A_0\) over X the family xu over \(X'\); a family of arrows \(s :X \rightarrow {(x_0, x_1)}^{*}A_1\) is reindexed to \(u^{*}s :X' \rightarrow {(u x_0, u x_1)}^{*}A_1\) by pulling back the section s along \((x_0, x_1)\). That gives a functor .
The above discussion leads to the following result.
Proposition 4
For \(\mathbf {A}\) an internal category in , there is an indexed category given by and .
Remark 2
Notice that the indexed category arising from an internal one is given by a strict functor (rather than merely a pseudofunctor). Then, evidently, internal categories yield rather special indexed categories, and not all indexed categories can be obtained from an internal one.
The construction extends to the monoidal context, as shown in the following proposition.
Proposition 5
Let \(\mathbf {V}\) be an internal monoidal category in . Then, is an indexed monoidal category on .
Proof
Let X be an object in . Then, has a monoidal structure induced by that of \(\mathbf {V}\). The monoidal product on objects is defined as
Then the monoidal product of arrows is given by the arrow
The monoidal unit is defined by the constant family indexed by X on the monoidal unit of \(\mathbf {V}\). The structural isomorphisms, associator and unitors are defined point-wise. Moreover, reindexing preserves the monoidal product. \(\square \)
A more conceptual explanation of Proposition 5, pointed out by the anonymous reviewer, is that is a finite product preserving 2-functor, and thus it preserves pseudomonoids.
Remark 3
The strictness of the monoidal products of the fibers of the indexed monoidal category obtained from an internal monoidal category \(\mathbf {V}\) is the same as that of the original monoidal product of \(\mathbf {V}\), so it will generally not be strict monoidal. Still, the reindexing functors for strictly preserve the monoidal structure, regardless of how strict the monoidal product of \(\mathbf {V}\) is. That means that the (actually strict) functor factorizes through the 2-category of (non-necessarily-strict) monoidal categories, strict monoidal functors and monoidal natural transformations. Such a category is quite uncommon, since normally there is little use for strict monoidal functors, especially between non-strict monoidal categories. Nonetheless, this shows that the indexed monoidal categories arising from internal monoidal categories are rather special ones.
Remark 4
For every internal category \(\mathbf {A}\), the fiber over an object X is enriched over :
Homset: .
Composition: .
Identity: .
Reindexing is compatible with this structure, in that the reindexing of the homset is the same as the homset of the reindexing. More explicitly, given a reindexing \(u :X' \rightarrow X\), by pullback-pasting we have that
$$\begin{aligned} u^{*}{(x_0, x_1)}^{*}A_1 \cong {(x_0 u, x_1 u)}^{*}A_1. \end{aligned}$$
In fact, the reindexing functor is a fully-faithful functor of enriched categories. Then is an indexed enriched category over the self-indexing of (see Example 1). Equivalently, it is the locally internal category over whose underlying indexed category is (up to natural isomorphism) as an indexed category [10, 16].
As stated in Theorem 1, indexed categories are equivalent to cloven fibrations. So, we can give an abstract definition of the externalization of an internal category as follows.
Definition 12
(externalization) The externalization of an internal category \(\mathbf {A}\) is the total category for the fibration associated to the indexed category . With abuse of notation, we denote the externalization of \(\mathbf {A}\) with , and context will usually suffice to distinguish between the use of the notation as a fibration or as an indexed category.
For practical purposes, it is useful to make the previous definition more explicit. The externalization of \(\mathbf {A}\) is the category given by the data
Objects: families of objects of \(\mathbf {A}\) indexed over objects of , that is, arrows \(X \rightarrow A_0\) with X in .
Morphisms: an arrow \((x :X \rightarrow A_0) \rightarrow (y :Y \rightarrow A_0)\) is given by a reindexing \(u :X \rightarrow Y\) and a family of arrows \(x \rightarrow yu\), that is, a section of the projection \(p :{(x, yu)}^{*}A_1 \rightarrow X\).
Composition: the composition is given by
Identity: the family of identity arrows.
Let \(F :\mathbf {A}\rightarrow \mathbf {B}\) be a functor of internal categories. Then, there is a functor of fibered categories defined on objects as
and on morphisms as
which restricts to a functor on the fibers .
Let \(\alpha :F \rightarrow G :\mathbf {A}\rightarrow \mathbf {B}\) be a natural transformation. Then, there is a natural transformation of fibered categories , defined as
which restricts to a natural transformation on the fibers .
Remark 5
If \(\mathbf {V}\) is a monoidal category in , then is an indexed monoidal category by Proposition 5. By Theorem 2, it follows that the externalization has an induced monoidal structure. Explicitly, the monoidal product on objects is given by
The monoidal product on arrows
$$\begin{aligned} (X \xrightarrow {x} V_0) \xrightarrow {\big ( X \xrightarrow {u} Y, X \xrightarrow {f} {(x, yu)}^{*}V_1 \big )} (Y \xrightarrow {y} V_0) \end{aligned}$$
and
$$\begin{aligned} (Z \xrightarrow {z} V_0) \xrightarrow {\big ( Z \xrightarrow {v} W, Z \xrightarrow {g} {(z, wv)}^{*}V_1 \big )} (W \xrightarrow {w} V_0) \end{aligned}$$
is the arrow indexed by and given by
The monoidal unit is . Finally, the structural isomorphisms are induced by those of \(\mathbf {V}\).
6 Internal Enriched Categories
We are finally ready to introduce the main topic of this paper: the theory of internal enrichment. We shall derive the necessary notions by the process of internalization of the theory of standard enrichment. Substantially, that amounts to translating the definitions from enriched category theory into the internal language of the ambient category. In other words, we take advantage of the fact that the axioms of the theory of enrichment are expressible in the internal language.
From now on, let \(\mathbf {V}\) be an internal monoidal category in . We define the notion of enrichment in \(\mathbf {V}\) internal to the ambient category , making use of the following notation to ease the use of the internal language in relation to internal categories, by bringing it closer to the standard notation of category theory. Given terms \(v :V_0\), \(w :V_0\) and \(f :V_1\), we write \(f :v \rightarrow w\) instead of (the conjunction of) the formulae and .
Definition 13
(internal enriched category) An internal \(\mathbf {V}\)-enriched category\(\mathbf {X}\) in , or \(\mathbf {V}\)-category, is given by the following data.
Underlying object: an object X of .
Internal hom: a morphism .
Composition: a morphism such that, in context \(x_0, x_1, x_2 :X\),
Identity: a morphism such that, in context \(x :X\),
Moreover, it has to satisfy the following axioms (in context \(x_0, x_1, x_2, x_3 :X\)).
×
Notice how the conventions on the internal language of allow one to express those axioms in a form very close to that used to define standard enriched categories.
Example 2
Let \(\mathscr {V}\) be a small monoidal category. Then, \(\mathscr {V}\) is an internal category in \({{\,\mathrm{Set}\,}}\), and internal \(\mathscr {V}\)-enriched categories in \({{\,\mathrm{Set}\,}}\) are standard (small) \(\mathscr {V}\)-enriched categories.
Continuing in the style of the previous definition, we give a notion of internal enriched functor, by translating the standard definition into the internal language.
Definition 14
(internal enriched functor) Let \(\mathbf {X}\) and \(\mathbf {Y}\) be \(\mathbf {V}\)-enriched categories. A \(\mathbf {V}\)-enriched functor, or \(\mathbf {V}\)-functor, \(F :\mathbf {X}\rightarrow \mathbf {Y}\) is given by the following data.
Objects component: an arrow \(F_0 :X \rightarrow Y\).
Morphisms component: an arrow \(F_1 :X \times X \rightarrow V_1\) such that, in context \(x_0, x_1 :X \),
Moreover, it has to satisfy the following axioms (in context \(x_0, x_1, x_2 :X\)).
×
We would expect the definition above to provide a category of internal \(\mathbf {V}\)-enriched categories and functors. We present the relevant data for that.
The composition of \(\mathbf {V}\)-functors \(F :\mathbf {X}\rightarrow \mathbf {Y}\) and \(G :\mathbf {Y}\rightarrow \mathbf {Z}\) is defined, in context \(x_0, x_1 :X\), as follows.
×
The identity \(\mathbf {V}\)-functor on \(\mathbf {X}\) is defined as follows.
It is just an exercise in the internal language to prove that the data so defined yield a category, as stated in the following proposition.
Proposition 6
Composition and identity of internal enriched functors strictly satisfy associativity and unitarity. Thus, \(\mathbf {V}\)-enriched categories and functors form a category .
Example 3
There is an underlying-object functor sending \(\mathbf {V}\)-enriched categories to their underlying object, and \(\mathbf {V}\)-enriched functors to their object-component.
Example 4
Let X be an object of . The indiscrete \(\mathbf {V}\)-enriched category \({{\,\mathrm{ind}\,}}(X)\) on X is given by
The rest of the structure follows from that. Analogously, a morphism \(f :X \rightarrow Y\) induces an indiscrete \(\mathbf {V}\)-enriched functor \({{\,\mathrm{ind}\,}}(f) :{{\,\mathrm{ind}\,}}(X) \rightarrow {{\,\mathrm{ind}\,}}(Y)\). Then, there is a functor .
Remark 6
To define the discrete \(\mathbf {V}\)-enriched category over an object of , we would need to assume some extra hypothesis. Firstly, we would need to be able to tell whether two elements of the underlying object of the \(\mathbf {V}\)-enriched category are equal. Secondly, we would need an initial object in \(\mathbf {V}\) to be the homset of non-equal elements of the underlying object. Both hypothesis do not hold in general. For example, the first one does not hold in the effective topos.
Finally, again by translating the standard definition into the internal language, we give the definition of internal enriched natural transformation.
Definition 15
(internal enriched natural transformation) Let \(\mathbf {X}\) and \(\mathbf {Y}\) be \(\mathbf {V}\)-enriched categories, and F and G be \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\). A \(\mathbf {V}\)-enriched natural transformation, or \(\mathbf {V}\)-natural transformation, \(\alpha :F \rightarrow G :\mathbf {X}\rightarrow \mathbf {Y}\) is given by an arrow \(\alpha :X \rightarrow V_1\) such that, in context \(x :X\),
and satisfying, in context \(x_0, x_1 :X\), the following axiom.
×
We would expect the definition above to provide a 2-category of internal \(\mathbf {V}\)-enriched categories, functors and natural transformations. We present the relevant data for that.
Consider \(\mathbf {V}\)-categories, \(\mathbf {V}\)-functors and \(\mathbf {V}\)-natural transformations as shown in the diagram:
Vertical composition of \(\mathbf {V}\)-natural transformations is defined, in context \(x :X\) by
The left whiskering is defined, in context \(w :W\), as \((\alpha L)(w) {:}{=}\alpha ( L_0(w) )\). The right whiskering is defined, in context \(x :X\), as follows.
The identity \(\mathbf {V}\)-natural transformation is defined as .
×
×
×
It is just an exercise in the internal language to prove that vertical composition and identity of internal enriched natural transformation strictly satisfy associativity and unitarity. Thus, a pair of \(\mathbf {V}\)-enriched categories yield a category of functors and natural transformations, as stated in the following proposition.
Proposition 7
Given \(\mathbf {V}\)-enriched categories \(\mathbf {X}\) and \(\mathbf {Y}\), the \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\) and natural transformations between them form a category .
Moreover, horizontal and vertical composition of \(\mathbf {V}\)-enriched natural transformations strictly satisfy the interchange laws, thus yielding an enrichment in . Equivalently, internal enriched categories, functors and natural transformations form a 2-category, as stated in the following result, whose proof is again an exercise in the internal language.
Proposition 8
\(\mathbf {V}\)-enriched categories, functors, and natural transformations form a strict 2-category .
By abuse of notation, we call both the category of \(\mathbf {V}\)-enriched categories and their functors, and the 2-category of \(\mathbf {V}\)-enriched categories, their functors and their natural transformations. As a consequence, given two \(\mathbf {V}\)-enriched categories \(\mathbf {X}\) and \(\mathbf {Y}\), we will denote by both the hom-set of \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\) and the hom-category of \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\) and their natural transformations. Context will usually suffice to determine in which sense the notation is being used.
Remark 7
Let \(\mathbf {X}\) be a \(\mathbf {V}\)-enriched category. There is an underlying -category \(U(\mathbf {X})\), such that \({U(\mathbf {X})}_0 {:}{=}X\) and \({U(\mathbf {X})}_1\) is the subobject of defined by the formula
(which can be explicitely defined via an equalizer) with the first and second projections as source and target. The composition is defined, in context , as follows.
Let \(F :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-enriched functor. There is an underlying functor \(U(F) :U(\mathbf {X}) \rightarrow U(\mathbf {Y})\) in , with \({U(F)}_0\) defined as \(F_0\) and \({U(F)}_1 (x_0, x_1, f)\), in context \((x_0, x_1, f) :{U(\mathbf {X})}_1\), as the tuple
in \({U(\mathbf {Y})}_1\).
Let \(\alpha :F \rightarrow G :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-enriched natural transformation. There is an underlying natural transformation \(U(\alpha ) :U(F) \rightarrow U(G) :U(\mathbf {X}) \rightarrow U(\mathbf {Y})\) in , defined, in context \(x :{U(\mathbf {X})}_0\) as \(U(\alpha )(x) {:}{=}\big ( F_0(x), G_0(x), \alpha (x) \big )\).
Those data yield the underlying-category-in- 2-functor .
We now consider the issue of the change of base. In this context, though, there are two sensible such notions, one coming from internal category theory and one from enriched category theory. Indeed, we can change both the ambient category and the enriching category.
To begin, let’s state the internal version of the standard result changing the enriching category.
Proposition 9
Let \(\mathbf {V}'\) be another monoidal category in , and \(F :\mathbf {V}\rightarrow \mathbf {V}'\) a monoidal functor. Then there is an induced 2-functor .
Proof
Let \(\mathbf {X}\) be a \(\mathbf {V}\)-category. Define a \(\mathbf {V}'\)-category \(F_\bullet (\mathbf {X})\) on X given by the following data.
Internal hom: .
Composition: .
Identity: .
Let \(G :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-functor. Define a \(\mathbf {V}'\)-functor \(F_\bullet (G) :F_\bullet (\mathbf {X}) \rightarrow F_\bullet (\mathbf {Y})\), with the same object component as G and arrow component given by \({(F_\bullet (G))}_1 {:}{=}F_1 G_1\).
Let \(\alpha :G \rightarrow G' :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-natural transformation. Define a \(\mathbf {V}'\)-natural transformation \(F_\bullet (\alpha ) :F_\bullet (G) \rightarrow F_\bullet (G') :F_\bullet (\mathbf {X}) \rightarrow F_\bullet (\mathbf {Y})\) as \(F_\bullet (\alpha ) {:}{=}F_1 \alpha \).
The axioms for the above definitions hold because of the functoriality of F. \(\square \)
Finally, let’s check that changing the ambient category induces a 2-functorial operation on internal enriched categories, just as it does on internal categories (see Proposition 2).
Proposition 10
Let be another finitely complete category and a functor preserving finite limits. By Proposition 3, there is an induced monoidal category \(F_\bullet (\mathbf {V})\) in . Then F induces a 2-functor .
Proof
Let \(\mathbf {X}\) be a \(\mathbf {V}\)-category. Define a \(F_\bullet (\mathbf {V})\)-category \(F_\bullet (\mathbf {X})\) on F(X) by applying the functor F to the structural arrows , and of \(\mathbf {X}\). That gives a \(F_\bullet (\mathbf {V})\)-enriched category because F preserves finite-limit logic, in terms of which internal enriched categories are defined. Analogously, define \(F_\bullet \) on \(\mathbf {V}\)-enriched functors and natural transformations. \(\square \)
7 Indexed Enriched Categories
In Sect. 4 we recalled the notion of indexed monoidal category. In [16], Shulman introduces a notion of enrichment over such a category which is a fibrational generalization of the standard enrichment. This comes in two versions: a general indexed version and a version which Shulman calls “small”. The latter is in a sense a hybrid notion, having an internal as well as an indexed aspect. We shall then compare both of them to internal enrichment, and find that they are closely related.
First, we give an outline of the notions of small -category, of functors between such categories, and of natural transformations between such functors. For brevity we will omit some diagrammatic axioms, referring to [16] for those. In this section, let be an -indexed monoidal category. Moreover, if \(f :B \rightarrow A\) is a morphism in and H is an object in , we shall write H(f) as a convenient notation for the object of .
Definition 16
(small -category) A small-category\(\mathbf {A}\) consists of the following data:
An object A of .
An object of .
A morphism where is the diagonal.
A morphism of
where are projections.
Moreover, it has to satisfy the associativity and unitarity axioms from [16].
Definition 17
(functor of small -categories) A functor of small -categories\(F :\mathbf {A}\rightarrow \mathbf {B}\) consists of the following data:
A morphism \(F_0 :A \rightarrow B\) of .
A morphism of .
Moreover, it has to satisfy the functoriality axioms from [16].
Definition 18
(natural transformation of small -categories) A natural transformation of small -categories\(\alpha :F \rightarrow G :\mathbf {A}\rightarrow \mathbf {B}\) consists of a morphism
We shall denote with the (2-)category of small -categories and their functors (and the natural transformation between those).
Recall from Sect. 5 that the externalization of an internal monoidal category \(\mathbf {V}\) is a monoidal indexed category over . Thus, we can investigate the relationship between \(\mathbf {V}\)-enriched categories and small -categories, and it turns out that they are the same thing in a very strict sense: their definitions coincide!
Proposition 11
To give a \(\mathbf {V}\)-enriched category (functor, natural transformation) is to give a small -category (functor, natural transformation). Thus, the 2-categories and are isomorphic.
Proof
A small -category \(\mathbf {X}\) is given by the following data:
An object X of .
An object of .
A morphism of
A morphism of
over , given by
Moreover, such data have to satisfy associativity and unitarity axioms. But these are precisely the same data that yield an internal \(\mathbf {V}\)-enriched category.
Analogously, to give a functor or a natural transformation of small -categories is to give a functor or a natural transformation of internal \(\mathbf {V}\)-enriched categories. \(\square \)
Now we present the notion of indexed category enriched in an indexed monoidal category [16]. For that, we shall extend a notation that we have consistently used in the internal context to standard enriched categories: if \(F :\mathscr {V}\rightarrow \mathscr {V}'\) is a lax monoidal functor and \(\mathscr {A}\) is a \(\mathscr {V}\)-enriched category, then \(F_{\bullet }(\mathscr {A})\) is the induced \(\mathscr {V}'\)-enriched category.
Definition 19
(indexed -category) An indexed -category\(\mathbf {B}\) consists of the following data:
For each X object of , a -category \(\mathbf {B}^{X}\).
For each \(f :X \rightarrow Y\) in , a fully faithful -functor \(f^{*} :{(f^*)}_{\bullet }( \mathbf {B}^{Y} )~\rightarrow ~\mathbf {B}^{X}\).
For each \(f :X \rightarrow Y\) and \(g :Y \rightarrow Z\) in , a -natural isomorphism (where we implicitly identify \({(f^{*})}_{\bullet } {(g^{*})}_{\bullet } \mathbf {B}^{Z}\) with \({(gf^{*})}_{\bullet } \mathbf {B}^{Z}\) in the domains of these functors).
For each X object of , a -natural isomorphism .
Moreover, for every \(f :X \rightarrow Y\), \(g :Y \rightarrow Z\) and \(h :Z \rightarrow K\) in , it has to satisfy the axioms for associativity and unitarity, analogous to those for ordinary indexed categories, by making the following diagrams of isomorphisms commute.
×
Definition 20
(functor of indexed -categories) An indexed-functor\(\mathscr {F} :\mathbf {B}\rightarrow \mathbf {B}'\) consists, for every object X of , of a -enriched functor \(\mathscr {F}^{X} :\mathbf {B}^{X} \rightarrow {\mathbf {B}'}^{X}\) together with, for every \(f :X \rightarrow Y\), an isomorphism . Such data have to satisfy the functoriality axioms by making the following diagrams of isomorphisms commute, for every \(f :X \rightarrow Y\) and \(g :Y \rightarrow Z\) in .
×
Definition 21
(natural transformation of indexed -categories) An indexed -natural transformation \(\alpha :\mathscr {F} \rightarrow \mathscr {G} :\mathbf {B}\rightarrow \mathbf {B}'\) consists, for every object X of , of a -natural transformation \(\alpha ^X :\mathscr {F}^X \rightarrow \mathscr {G}^X :\mathbf {B}^X \rightarrow {\mathbf {B}'}^X\), satisfying naturality axioms by making the following diagram commute, for every \(f :X \rightarrow Y\).
×
With the data thus defined (plus the obvious notions of compositions and identities) we can define a 2-category of indexed enriched categories.
Definition 22
(category of indexed -categories) We denote with the 2-category of indexed -categories, their functors and the natural transformations between them.
By abuse of notation, we shall denote with also the mere 1-category of indexed -categories and their functors. Usually, the context is sufficient to distinguish when the notation is being used referring to the 1-category or the 2-category.
In general, embeds into as a full sub-2-category (even though this fact is omitted from [16] and, according to the author’s knowledge, not addressed in the literature at large). Of course, since and are isomorphic by Proposition 11, is a full sub-2-category of as well. We will now describe concretely the 2-embedding .
First, let \(\mathbf {X}\) be a \(\mathbf {V}\)-enriched category and let us define an indexed -category . Given an indexing object I of , define the -enriched category as follows:
Objects: I-indexed families \(x :I \rightarrow X\) of elements of X.
Internal hom: .
Composition: .
Identity: .
Let \(f :I \rightarrow J\) be a re-indexing. Define the -functor as follows.
Since \(f^*_1(x_0, x_1)\) is the identity of as an object of , then \(f^*\) is full and faithful, as required by the definition. The rest of the structure is given by canonical isomorphisms verifying the axioms.
Secondly, let \(F :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-enriched functor and let us define an indexed -functor induced by F. For an indexing object I, define the -enriched functor as follows:
Objects component: .
Morphisms component: .
Notice that, for any reindexing \(f :I \rightarrow J\), we have an equality , meaning that the axioms for indexed -functors are automatically satisfied.
Finally, let \(\alpha :F \rightarrow G :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-enriched natural transformation and let us define an indexed -natural transformation induced by \(\alpha \). Let I be an indexing object and define the -enriched natural transformation as . The naturality condition for indexed -natural transformations is trivially satisfied because the defining isomorphisms of indexed -functors and are identities.
Remark 8
Indexed -categories don’t canonically induce internal \(\mathbf {V}\)-enriched categories. In particular, the categories are small, as their object of objects is the homset , but that is not generally the case for indexed -categories.
To conclude, we look at the interplay between externalizations and the underlying categories (see Remark 7 for the definition of underlying internal category of an internal enriched category).
Proposition 12
Let \(\mathbf {X}\) be a \(\mathbf {V}\)-enriched category. Then, there is a natural isomorphism of indexed categories between the underlying indexed category of the indexed -category and the externalization of the underlying -category \(U(\mathbf {X})\).
Proof
Let I be an indexing object. We need to prove that there is an isomorphism between the underlying standard category of the -enriched category and the fiber over I of the externalization of the underlying -category \(U(\mathbf {X})\). Moreover, for any reindexing \(f :J \rightarrow I\) in , the square
has to commute.
×
For both categories, the objects are I-indexed families of objects of \(\mathbf {X}\), and the arrows \((I \xrightarrow {x_0} X) \rightarrow (I \xrightarrow {x_1} X)\) are the sections of the projection
so that the categories are clearly isomorphic to each other, and the square commutes trivially. \(\square \)
The previous result can be extended to the following proposition.
Proposition 13
The following diagram of 2-functors commutes.
×
The above discussion suggests that the indexed -category should yield a notion of externalization of an internal enriched category \(\mathbf {X}\). That would be defined as the large -category obtained by via the functor \(\Theta \) [16, Section 6], analogously to how one gets the total category of an indexed category via the Grothendieck construction (Theorem 1).
Acknowledgements
I wish to thank the Cambridge Trust and the EPSRC, for generously funding the doctoral research resulting in the material contained in this paper. I also wish to acknowledge and thank my doctoral supervisor, Professor Martin Hyland, for the supervision and the guidance offered on mathematical and academic matters in the course of said research activity; Professor Giuseppe Rosolini, for the original suggestion to enrich in the internal category of modest sets which inspired this work; and Dr. Alessio D’Alì, for kindly providing valuable feedback and suggestions on the paper’s draft.
Declarations
Conflict of interest
The authors declare that they have no conflict of interest.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
be a category with finite limits, which we regard as our ambient category. To be precise, in particular we require
to have a cartesian monoidal structure, that is, a monoidal structure given by a functorial choice of binary products
and a chosen terminal object
. As a category with finite limits,
is a model for cartesian logic, or finite limit logic. We will frequently use the internal language of
to ease the notation, although in an informal style. At the cost of readability, the given formulas could be elaborated either into the language of Freyd’s essentially algebraic theories [2], or into Johnstone’s cartesian logic [10], or into the partial Horn logic of Palmgren and Vickers [12], other than into commutative diagrams.
.
is a diagram 
(where
is the pullback of
and
) satisfying the usual axioms for categories, which can be expressed in the internal language of
by the formulae
where
is the pullback of
and
, and
is the iterated pullback. Notice that, by the universal property of the pullback,
if and only if \(f :A_1\), \(g :A_1\), and
, in the sense that local sections
correspond bijectively to pairs of local sections \(f, g :X \rightarrow A_1\) such that
.
.
. A functor of internal categories \(F :\mathbf {A}\rightarrow \mathbf {B}\) is given by a pair of arrows \(F_0 :A_0 \rightarrow B_0\) and \(F_1 :A_1 \rightarrow B_1\) such that
The composition
(shortened in GF for brevity) of two consecutive internal functors \(F :\mathbf {A}\rightarrow \mathbf {B}\) and \(G :\mathbf {B}\rightarrow \mathbf {C}\), and the identity functor
for an internal category \(\mathbf {A}\), are defined in the usual way.
.
has finite limits induced point-wise by the corresponding limits in
. In particular, there is a terminal internal category
and a binary product
of internal categories making
a cartesian monoidal category.
be another category with finite limits, and
a functor preserving finite limits. Then, there is a change-of-base functor
applying F to the underlying graph of internal categories. In the following remark, we notice some useful properties of
in relation to slicing and change of base.
. Then, there is an adjunction
where the functor
is given by post-composition with i, and the functor
is given by pullback along i. This adjunction extends to internal categories, yielding
. In particular, the unique arrow
yields an adjunction
.
be a functor between categories with finite limits which preserves such finite limits. Then, the induced change-of-base functor
preserves finite limits.
sending an internal category to its underlying object-of-objects. This functor preserves the cartesian monoidal structure. We then mention a few remarkable examples of internal categories:Then, we have the following adjunctions:An alternative, more abstract way to look at the discrete category with respect to Remark 1 is to notice that \({{\,\mathrm{dis}\,}}A\) is (isomorphic to)
.
.
.
(denoted in the same way as its underlying 1-category with abuse of notation; context usually suffices to distinguish whether we are referring to the underlying 1-category or the 2-category).
. A natural transformation of internal functors \(\alpha :F \rightarrow G :\mathbf {A}\rightarrow \mathbf {B}\) is given by an arrow \(\alpha :A_0 \rightarrow B_1\) such that
Vertical and horizontal compositions of natural transformations and the identity natural transformation are defined in the usual way.
denotes the identity of the category \(\mathbf {A}\), while
denotes the identity functor on \(\mathbf {A}\) and
denotes the identity natural transformation on \(F :\mathbf {A}\rightarrow \mathbf {B}\). When it is clear from the context, we might omit the subscript of
and write, for example,
in place of
and
in place of
.
, of the notions of monoidal category, functor and natural transformation.
equipped with functorsand natural isomorphismssuch that, in context \(a, b, c, d :V_0\), the axioms 
. For example, Equation 1 represents the following formula.
Such translation is straightforward, but we favour the diagrammatic representation as it is more intuitive and familiar to the category theorist.
, and
,
,
, and
,
must be pseudomonoids in the 2-category
, which is what our definition amounts to.
is given by an internal functor
and coherence natural isomorphisms
and
such that, in context \(a, b, c :V_0\), the axioms 
is a natural transformation
such that, in context \(a, b, :V_0\), the axioms 
form a category
. Moreover, monoidal natural transformations in
give
the structure of a 2-category (denoted in the same way as its underlying 1-category with abuse of notation; context usually suffices to distinguish whether we are referring to the underlying 1-category or the 2-category).
be a functor between categories with finite limits which preserves such finite limits. Then, there is an induced change-of-base functor
, which also preserves finite limits.
sending monoidal categories, functors and natural transformations to, respectively, their underlying internal categories, functors and natural transformations.
-indexed category is a pseudofunctor
, where
is the 2-category of categories, functors, and natural transformations.
is the
-indexed category whose fiber over an object X is the slice category
and where the reindexing along \(f :X \rightarrow Y\) is given by pullback along f.
if, for any other arrow \(h :A'' \rightarrow A\) in \(\mathscr {F}\) and \(g :P(A'') \rightarrow P(A')\) in
such that \(P(l) g = P(h)\), there exists a unique \(k :A'' \rightarrow A'\) in \(\mathscr {F}\) such that \(l k = h\) and \(P(k) = g\).
is a fibration if for any A in \(\mathscr {F}\) and \(f :X \rightarrow P(A)\) there is a cartesian arrow \(l :A' \rightarrow A\) such that \(P(l) = f\), called the cartesian lifting of f. Moreover, a fibration is cloven if it comes with a choice of cartesian liftings.
-indexed category
is, via the Grothendieck construction, equivalent to a cloven fibration
. More precisely, there is an equivalence of bicategories
(and, in fact, an equivalence of strict 2-categories [10]), where
is the 2-category of cloven fibrations over
, strong morphisms of fibrations, and transformations of fibrations.
-indexed monoidal category is a pseudofunctor
, where
is the 2-category of monoidal categories, strong monoidal functors, and monoidal transformations.
such that the underlying functor is strict monoidal (with
regarded as cartesian monoidal) and the tensor product in \(\mathscr {V}\) preserves cartesian arrows.
is an
-indexed monoidal category, then, in the cloven fibration
, it is evident that
has tensor products only for objects in the same fiber, and the result is still an object in that fiber. On the other hand, if
is a monoidal fibration, and A and B are objects of \(\mathscr {V}\) lying over the objects X and Y of
respectively, then the tensor product
lies over
. However, in case the monoidal structure on
is given by the product, i.e.,
is cartesian monoidal, such as our ambient category
is, then there is a correspondence (for details, see Theorem 12.7 from [15]). We recall this result in the following theorem.
-indexed monoidal category
is, via the Grothendieck construction, equivalent to a monoidal fibration
. More precisely, there is an equivalence of bicategories
, where
is the 2-category of monoidal fibrations over
, strong monoidal morphisms of fibrations, and monoidal transformations of fibrations.
and X an object of
. We regard an arrow \(X \rightarrow A_0\) as representing an indexed family of objects of \(\mathbf {A}\) over the indexing object X. Given two such indexed families \(x_0, x_1 :X \rightarrow A_0\), consider the pullback 
inducing a composition of indexed families of arrows: given two families of arrows \(s_0 :X \rightarrow {(x_0, x_1)}^{*}A_1\) and \(s_1 :X \rightarrow {(x_1, x_2)}^{*}A_1\), their composition is defined as
Moreover, a family of objects \(x :X \rightarrow A_0\) induces a family of identity arrows
. These data form the category
of indexed families of objects and morphisms of \(\mathbf {A}\) over X.
.
, there is an indexed category
given by
and
.
(rather than merely a pseudofunctor). Then, evidently, internal categories yield rather special indexed categories, and not all indexed categories can be obtained from an internal one.
. Then,
is an indexed monoidal category on
.
. Then,
has a monoidal structure induced by that of \(\mathbf {V}\). The monoidal product on objects is defined as
To define the monoidal product of arrows, letandbe arrows of
, and notice that
restricts to
Then the monoidal product of arrows
is given by the arrow
The monoidal unit
is defined by the constant family indexed by X on the monoidal unit of \(\mathbf {V}\). The structural isomorphisms, associator and unitors are defined point-wise. Moreover, reindexing preserves the monoidal product. \(\square \)
is a finite product preserving 2-functor, and thus it preserves pseudomonoids.
obtained from an internal monoidal category \(\mathbf {V}\) is the same as that of the original monoidal product of \(\mathbf {V}\), so it will generally not be strict monoidal. Still, the reindexing functors for
strictly preserve the monoidal structure, regardless of how strict the monoidal product of \(\mathbf {V}\) is. That means that the (actually strict) functor
factorizes through the 2-category of (non-necessarily-strict) monoidal categories, strict monoidal functors and monoidal natural transformations. Such a category is quite uncommon, since normally there is little use for strict monoidal functors, especially between non-strict monoidal categories. Nonetheless, this shows that the indexed monoidal categories arising from internal monoidal categories are rather special ones.
over an object X is enriched over
:Reindexing is compatible with this structure, in that the reindexing of the homset is the same as the homset of the reindexing. More explicitly, given a reindexing \(u :X' \rightarrow X\), by pullback-pasting we have thatIn fact, the reindexing functor
is a fully-faithful functor of enriched categories. Then
is an indexed enriched category over the self-indexing of
(see Example 1). Equivalently, it is the locally internal category over
whose underlying indexed category is (up to natural isomorphism)
as an indexed category [10, 16].
.
.
.
. With abuse of notation, we denote the externalization of \(\mathbf {A}\) with
, and context will usually suffice to distinguish between the use of the notation as a fibration or as an indexed category.
defined on objects as
and on morphisms as
which restricts to a functor on the fibers
.
, that is, arrows \(X \rightarrow A_0\) with X in
.
, defined as
which restricts to a natural transformation on the fibers
.
, then
is an indexed monoidal category by Proposition 5. By Theorem 2, it follows that the externalization
has an induced monoidal structure. Explicitly, the monoidal product on objects is given by
The monoidal product on arrowsandis the arrow
indexed by
and given by
The monoidal unit is
. Finally, the structural isomorphisms are induced by those of \(\mathbf {V}\).
. We define the notion of enrichment in \(\mathbf {V}\) internal to the ambient category
, making use of the following notation to ease the use of the internal language in relation to internal categories, by bringing it closer to the standard notation of category theory. Given terms \(v :V_0\), \(w :V_0\) and \(f :V_1\), we write \(f :v \rightarrow w\) instead of (the conjunction of) the formulae
and
.
, or \(\mathbf {V}\)-category, is given by the following data.Moreover, it has to satisfy the following axioms (in context \(x_0, x_1, x_2, x_3 :X\)). 
.
.
such that, in context \(x_0, x_1, x_2 :X\), 
such that, in context \(x :X\), 
allow one to express those axioms in a form very close to that used to define standard enriched categories.
of internal \(\mathbf {V}\)-enriched categories and functors. We present the relevant data for that.
on \(\mathbf {X}\) is defined as follows.
It is just an exercise in the internal language to prove that the data so defined yield a category, as stated in the following proposition.
.
sending \(\mathbf {V}\)-enriched categories to their underlying object, and \(\mathbf {V}\)-enriched functors to their object-component.
. The indiscrete \(\mathbf {V}\)-enriched category \({{\,\mathrm{ind}\,}}(X)\) on X is given by
The rest of the structure follows from that. Analogously, a morphism \(f :X \rightarrow Y\) induces an indiscrete \(\mathbf {V}\)-enriched functor \({{\,\mathrm{ind}\,}}(f) :{{\,\mathrm{ind}\,}}(X) \rightarrow {{\,\mathrm{ind}\,}}(Y)\). Then, there is a functor
.
, we would need to assume some extra hypothesis. Firstly, we would need to be able to tell whether two elements of the underlying object of the \(\mathbf {V}\)-enriched category are equal. Secondly, we would need an initial object in \(\mathbf {V}\) to be the homset of non-equal elements of the underlying object. Both hypothesis do not hold in general. For example, the first one does not hold in the effective topos.
and satisfying, in context \(x_0, x_1 :X\), the following axiom. 
is defined, in context \(x :X\) by 
is defined, in context \(w :W\), as \((\alpha L)(w) {:}{=}\alpha ( L_0(w) )\). The right whiskering
is defined, in context \(x :X\), as follows. 
is defined as
.
.
. Equivalently, internal enriched categories, functors and natural transformations form a 2-category, as stated in the following result, whose proof is again an exercise in the internal language.
.
both the category of \(\mathbf {V}\)-enriched categories and their functors, and the 2-category of \(\mathbf {V}\)-enriched categories, their functors and their natural transformations. As a consequence, given two \(\mathbf {V}\)-enriched categories \(\mathbf {X}\) and \(\mathbf {Y}\), we will denote by
both the hom-set of \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\) and the hom-category of \(\mathbf {V}\)-enriched functors \(\mathbf {X}\rightarrow \mathbf {Y}\) and their natural transformations. Context will usually suffice to determine in which sense the notation is being used.
-category \(U(\mathbf {X})\), such that \({U(\mathbf {X})}_0 {:}{=}X\) and \({U(\mathbf {X})}_1\) is the subobject of
defined by the formula
(which can be explicitely defined via an equalizer) with the first and second projections as source and target. The composition is defined, in context
, as follows.
Let \(F :\mathbf {X}\rightarrow \mathbf {Y}\) be a \(\mathbf {V}\)-enriched functor. There is an underlying functor \(U(F) :U(\mathbf {X}) \rightarrow U(\mathbf {Y})\) in
, with \({U(F)}_0\) defined as \(F_0\) and \({U(F)}_1 (x_0, x_1, f)\), in context \((x_0, x_1, f) :{U(\mathbf {X})}_1\), as the tuple
in \({U(\mathbf {Y})}_1\).
, defined, in context \(x :{U(\mathbf {X})}_0\) as \(U(\alpha )(x) {:}{=}\big ( F_0(x), G_0(x), \alpha (x) \big )\).
2-functor
.
, and \(F :\mathbf {V}\rightarrow \mathbf {V}'\) a monoidal functor. Then there is an induced 2-functor
.
.
.
.
be another finitely complete category and
a functor preserving finite limits. By Proposition 3, there is an induced monoidal category \(F_\bullet (\mathbf {V})\) in
. Then F induces a 2-functor
.
,
and
of \(\mathbf {X}\). That gives a \(F_\bullet (\mathbf {V})\)-enriched category because F preserves finite-limit logic, in terms of which internal enriched categories are defined. Analogously, define \(F_\bullet \) on \(\mathbf {V}\)-enriched functors and natural transformations. \(\square \)
-category, of functors between such categories, and of natural transformations between such functors. For brevity we will omit some diagrammatic axioms, referring to [16] for those. In this section, let
be an
-indexed monoidal category. Moreover, if \(f :B \rightarrow A\) is a morphism in
and H is an object in
, we shall write H(f) as a convenient notation for the object
of
.
-category) A small
-category \(\mathbf {A}\) consists of the following data:where
are projections.
.
of
.
where
is the diagonal.
-categories) A functor of small
-categories \(F :\mathbf {A}\rightarrow \mathbf {B}\) consists of the following data:Moreover, it has to satisfy the functoriality axioms from [16].
.
of
.
-categories) A natural transformation of small
-categories \(\alpha :F \rightarrow G :\mathbf {A}\rightarrow \mathbf {B}\) consists of a morphism
satisfying the naturality axiom from [16].
the (2-)category of small
-categories and their functors (and the natural transformation between those).
over
. Thus, we can investigate the relationship between \(\mathbf {V}\)-enriched categories and small
-categories, and it turns out that they are the same thing in a very strict sense: their definitions coincide!
-category (functor, natural transformation). Thus, the 2-categories
and
are isomorphic.
-category \(\mathbf {X}\) is given by the following data:Moreover, such data have to satisfy associativity and unitarity axioms. But these are precisely the same data that yield an internal \(\mathbf {V}\)-enriched category.
.
of
.
over
, given by 
-categories is to give a functor or a natural transformation of internal \(\mathbf {V}\)-enriched categories. \(\square \)
-category) An indexed
-category \(\mathbf {B}\) consists of the following data:Moreover, for every \(f :X \rightarrow Y\), \(g :Y \rightarrow Z\) and \(h :Z \rightarrow K\) in
, it has to satisfy the axioms for associativity and unitarity, analogous to those for ordinary indexed categories, by making the following diagrams of isomorphisms commute. 
, a
-category \(\mathbf {B}^{X}\).
, a fully faithful
-functor \(f^{*} :{(f^*)}_{\bullet }( \mathbf {B}^{Y} )~\rightarrow ~\mathbf {B}^{X}\).
, a
-natural isomorphism
(where we implicitly identify \({(f^{*})}_{\bullet } {(g^{*})}_{\bullet } \mathbf {B}^{Z}\) with \({(gf^{*})}_{\bullet } \mathbf {B}^{Z}\) in the domains of these functors).
, a
-natural isomorphism
.
-categories) An indexed
-functor \(\mathscr {F} :\mathbf {B}\rightarrow \mathbf {B}'\) consists, for every object X of
, of a
-enriched functor \(\mathscr {F}^{X} :\mathbf {B}^{X} \rightarrow {\mathbf {B}'}^{X}\) together with, for every \(f :X \rightarrow Y\), an isomorphism
. Such data have to satisfy the functoriality axioms by making the following diagrams of isomorphisms commute, for every \(f :X \rightarrow Y\) and \(g :Y \rightarrow Z\) in
. 
-categories) An indexed
-natural transformation \(\alpha :\mathscr {F} \rightarrow \mathscr {G} :\mathbf {B}\rightarrow \mathbf {B}'\) consists, for every object X of
, of a
-natural transformation \(\alpha ^X :\mathscr {F}^X \rightarrow \mathscr {G}^X :\mathbf {B}^X \rightarrow {\mathbf {B}'}^X\), satisfying naturality axioms by making the following diagram commute, for every \(f :X \rightarrow Y\). 
-categories) We denote with
the 2-category of indexed
-categories, their functors and the natural transformations between them.
also the mere 1-category of indexed
-categories and their functors. Usually, the context is sufficient to distinguish when the notation is being used referring to the 1-category or the 2-category.
embeds into
as a full sub-2-category (even though this fact is omitted from [16] and, according to the author’s knowledge, not addressed in the literature at large). Of course, since
and
are isomorphic by Proposition 11,
is a full sub-2-category of
as well. We will now describe concretely the 2-embedding
.
-category
. Given an indexing object I of
, define the
-enriched category
as follows:Let \(f :I \rightarrow J\) be a re-indexing. Define the
-functor
as follows.
Since \(f^*_1(x_0, x_1)\) is the identity of
as an object of
, then \(f^*\) is full and faithful, as required by the definition. The rest of the structure is given by canonical isomorphisms verifying the axioms.
.
.
.
-functor
induced by F. For an indexing object I, define the
-enriched functor
as follows:Notice that, for any reindexing \(f :I \rightarrow J\), we have an equality
, meaning that the axioms for indexed
-functors are automatically satisfied.
.
.
-natural transformation
induced by \(\alpha \). Let I be an indexing object and define the
-enriched natural transformation
as
. The naturality condition for indexed
-natural transformations is trivially satisfied because the defining isomorphisms of indexed
-functors
and
are identities.
-categories don’t canonically induce internal \(\mathbf {V}\)-enriched categories. In particular, the categories
are small, as their object of objects is the homset
, but that is not generally the case for indexed
-categories.
between the underlying indexed category of the indexed
-category
and the externalization of the underlying
-category \(U(\mathbf {X})\).
between the underlying standard category of the
-enriched category
and the fiber over I of the externalization of the underlying
-category \(U(\mathbf {X})\). Moreover, for any reindexing \(f :J \rightarrow I\) in
, the square 
so that the categories are clearly isomorphic to each other, and the square commutes trivially. \(\square \)
-category
should yield a notion of externalization of an internal enriched category \(\mathbf {X}\). That would be defined as the large
-category obtained by
via the functor \(\Theta \) [16, Section 6], analogously to how one gets the total category of an indexed category via the Grothendieck construction (Theorem 1).