natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In set-level foundations, there are two ways to compare two objects of a category for sameness: by equality or by isomorphism. The principle of equivalence argues that isomorphism is the “correct” notion of “sameness” for objects of a category, but the notion of equality is still present to be ignored.
Note that even in a skeletal category, where the mere property of “being isomorphic” coincides with the property of “being equal”, one cannot collapse the notions of isomorphism and equality because an object can still be isomorphic to itself in more than one way. This distinction only disappears in a gaunt category, but not every category is equivalent to a gaunt one.
By contrast, in higher foundations, it is possible to expand the notion of “equality” so that it coincides with isomorphism: just as two objects can be isomorphic in more than one way, they can also be equal in more than one way. The notion of “category” in which equality and isomorphism coincide in this way is called univalent or saturated. This is an analogue for 1-categories of imposing antisymmetry on a preordered set (a.k.a. a (0,1)-category) to obtain a partially ordered set (a.k.a. a skeletal or gaunt (0,1)-category).
Since we are talking about 1-categories whose hom-types are h-sets, in a univalent category the type of objects is a 1-type. By contrast, a “precategory” in higher foundations maintains equality of objects (which can have arbitrary h-level) as separate from isomorphism, while a “strict category” requires that the type of objects form a set.
We work in a dependent type theory with some notion of identity type or path type, denoted $a=b$. If $A$ is a precategory and $a,b:ob(A)$, we write $a\cong b$ for the type of isomorphisms from $a$ to $b$.
There is a map
By induction on identity, we may assume $a$ and $b$ are the same. But then we have $1_a:hom_A(a,a)$, which is clearly an isomorphism.
A univalent category or saturated category is a precategory which is Rezk complete, meaning that the above canonical function
an equivalence of types.
In homotopy type theory, univalent categories are arguably the best notion of “category”. Specifically, in HoTT/UF:
For these reasons, some of the HoTT/UF literature (including the HoTT Book) refers to univalent categories as simply “categories”.
The situation in plain intensional type theory is less clear, since without the univalence axiom, naturally-occurring precategories cannot be shown to be univalent (or strict) and the Rezk completion need not exist. Thus, in this case precategories seem unavoidable. Fortunately, a surprising amount of category theory can be developed with precategories.
(To be completely precise, the notion of “univalent category” can also be defined in set-level foundations. In that case it turns out to be equivalent to the notion of gaunt category, which again is not satisfactory as a general notion of “category”. More generally, a strict category is univalent if and only if it is gaunt.)
On this page we will not use the plain term “category” at all, but speak only of “precategories”, “univalent categories”, and “strict categories”.
Most nLab pages about category theory are, and should remain, written in a fairly foundation-agnostic way. If the reader is interpreting them in HoTT/UF, it is usually best to read “category” as meaning “univalent category” for the reasons above. However, in many cases it is also possible to read it as meaning “precategory” or “strict category”, as would be necessary if interpreting them in plain intensional type theory.
It is not usually necessary for pages about ordinary category theory to remark on this issue at all. However, if there are subtleties regarding the choice of interpretation (e.g. if some construction, such as a Kleisli category, may lead out of the world of univalent categories; or if some structure, such as a dagger category, requires changing the notion of “univalence”), it is appropriate to include a remark. Such a remark should generally be lower down on the page, not at the top, so that it doesn’t confuse first-time readers.
Note: All categories given can become univalent via the Rezk completion.
As noted above, every gaunt category is a strict univalent category, or equivalently a skeletal univalent category.
There is a precategory Set, whose type of objects is $Set$, and with $hom_{Set}(A,B)\equiv (A \to B)$. The univalence axiom implies that this is a univalent category. One can also show from this that any precategory of set-level structures such as groups, rings topological spaces, etc. is also univalent.
For any 1-type $X$, there is a univalent category with $X$ as its type of objects and with $hom(x,y)\equiv(x=y)$. If $X$ is a set we call this the discrete category on $X$. In general, we call it a (univalent) groupoid.
More generally, or any type $X$, there is a precategory with $X$ as its type of objects and with $hom(x,y)\equiv \| x= y \|_0$. The composition operation
is defined by induction on truncation from concatenation of the identity type. We call this the fundamental pregroupoid of $X$. It is univalent if and only if $X$ is a 1-type; its Rezk completion is the fundamental (univalent) groupoid of $X$.
There is a precategory whose type of objects is the type universe $\mathcal{U}$ and with $hom(X,Y)\equiv \| X \to Y\|_0$, and composition defined by induction on truncation from ordinary composition of functions. We call this the homotopy precategory of types; it is not univalent (although it contains the univalent category Set as a sub-precategory).
Given two categories $A$ and $B$, if $B$ is univalent, then the functor category $B^A$ is univalent.
Let $F:A \to B$ and $G:A \to B$ be functors from $A$ to $B$.
Suppose that $\gamma:F \to G$ is a natural isomorphism. Then for any object $a : Ob(A)$, there is an isomorphism $\gamma_a: F_{ob}(a) \cong G_{ob}(a)$ in $B$. Since $B$ is univalent, this shows that $F_{ob}(a) = G_{ob}(a)$ for all objects $a$, and by function extensionality, that $F_{ob} = G_{ob}$.
Now, for any $a : Ob(A)$ and $b : Ob(B)$, the functions $F_{mor}(a,b):Mor_A(a,b) \to Mor_B(F_{ob}(a),F_{ob}(b))$ and $G_{mor}(a,b):Mor_A(a,b) \to Mor_B(G_{ob}(a),G_{ob}(b))$ are equal, because we established above that $F(a) = G(a)$ for all $a : Ob(a)$. Because the object functions and morphism functions of $F$ and $G$ are equal to each other, $F = G$.
Thus, if there is an isomorphism $\gamma:F \cong G$, then $F = G$.
this proof needs to be revised since it is missing the explicit identifications
An equivalent-on-objects functor between two precategories $A$ and $B$ is a functor $F:A \to B$ where the object function $F_{ob}:Ob(A) \to Ob(B)$ is a equivalence of types.
A split essentially surjective functor between $A$ and $B$ is a functor $F:A \to B$ where for every object $b : Ob(B)$, there is a specified object $a : Ob(A)$ and an isomorphism $f:F_{ob}(a) \cong b$.
A fully faithful functor is a functor $F:A\to B$ such that each map on hom-sets $F_{a,b} : A(a_0,a_1) \to B(F(a_0),F(a_1))$ is an equivalence of types.
These definitions are important for defining the two notions of equality for categories:
An isomorphism of categories is a fully faithful equivalent-on-objects functor.
An equivalence of categories is a fully faithful split essentially surjective functor. Equivalently, it is a functor $F:A \to B$ which has a left adjoint $G:B \to A$ such that the unit $\eta:1_A \to G F$ and counit $\epsilon:F G \to 1_B$ are isomorphisms.
For univalent categories, isomorphism of categories and equivalence of categories coincide.
…
In a univalent category, the type of objects is a 1-type.
It suffices to show that for any $a,b:A$, the type $a=b$ is a set. But $a=b$ is equivalent to $a \cong b$ which is a set.
There is a canonical way to turn a category into a univalent category via the Rezk completion.
The relation between Segal completeness (now often “Rezk completeness”) for internal categories in HoTT and the univalence axiom had been pointed out in
A comprehensive discussion for 1-categories then appeared in:
Exposition:
Amélia Liao, Univalent Category Theory, Homotopy Type Theory Electronic Seminar Talks, (October 2022) [video]
Implementation in Coq:
Coq code formalizing this includes the following:
and in cubical Agda:
Generalization to (n,1)-categories is discussed in
and, by different means, in
Emily Riehl, Michael Shulman, A type theory for synthetic $\infty$-categories (arXiv:1705.07442)
Emily Riehl, The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories, talk at Vladimir Voevodsky Memorial Conference 2018 (pdf)
Formalization of bicategories:
Lemmas and proofs above are taken from:
On monoidal univalent categories:
A formalization in HoTT-Agda of general (n,r)-categories for $n,r \in \mathbb{N} \sqcup \{\infty\}$, defined as coinductive types of infinity-graphs, with operations defined by induction-coinduction, is implemented in
Last revised on May 26, 2023 at 21:16:19. See the history of this page for a list of all contributions to it.