ncatlab.org

univalent category in nLab

Contents

Context

Category theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

homotopy levels

semantics

Contents

Idea

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.

Definition

We work in a dependent type theory with some notion of identity type or path type, denoted a=ba=b. If AA is a precategory and a,b:ob(A)a,b:ob(A), we write a≅ba\cong b for the type of isomorphisms from aa to bb.

Lemma

There is a map

idtoiso:(a=b)→(a≅b)idtoiso : (a=b) \to (a \cong b)

Proof

By induction on identity, we may assume aa and bb are the same. But then we have 1 a:hom A(a,a)1_a:hom_A(a,a), which is clearly an isomorphism.

Definition

A univalent category or saturated category is a precategory which is Rezk complete, meaning that the above canonical function

idtoiso:(a=b)→(a≅b)idtoiso : (a=b) \to (a \cong b)

an equivalence of types.

Comparing notions of category

In homotopy type theory, univalent categories are arguably the best notion of “category”. Specifically, in HoTT/UF:

  1. Most naturally occurring precategories are in fact univalent categories, such as the category Set and most categories of structured objects built from it such as Grp, Ring, Vect, Mod, Top, Met, StrCat, etc.
  2. Furthermore, every precategory is weakly equivalent to a univalent category (its Rezk completion).
  3. The theory of univalent categories is abstractly nicer than that of either precategories or strict categories. For instance, the statement “a fully faithful and essentially surjective functor is an equivalence” for strict categories is equivalent to the axiom of choice, for precategories it is just false, and for univalent categories it is just true. (On the other hand it can be argued that one should be using split essentially surjective functors instead of essentially surjective functors, since every equivalence of precategories is fully faithful and split essentially surjective.)
  4. Under the semantics of HoTT/UF in (infinity,1)-toposes, univalent categories are interpreted by the correct notion of stacks of 1-categories. (See relation between type theory and category theory and category object in an (infinity,1)-category.) This is not true for either precategories or strict categories. (Although in the “classical” model in ∞Gpd, univalent categories are interpreted by 1-truncated complete Segal spaces, while strict categories are interpreted by 1-truncated Segal categories and precategories are interpreted by 1-truncated Segal spaces. Thus, in this model only, strict categories also give a correct notion of “category”, although precategories still do not.)

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”.

Examples

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 SetSet, and with hom Set(A,B)≡(A→B)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 XX, there is a univalent category with XX as its type of objects and with hom(x,y)≡(x=y)hom(x,y)\equiv(x=y). If XX is a set we call this the discrete category on XX. In general, we call it a (univalent) groupoid.

  • More generally, or any type XX, there is a precategory with XX as its type of objects and with hom(x,y)≡‖x=y‖ 0hom(x,y)\equiv \| x= y \|_0. The composition operation

    ‖y=z‖ 0→‖x=y‖ 0→‖y=z‖ 0\|y=z\|_0 \to \|x=y\|_0 \to \|y=z\|_0

    is defined by induction on truncation from concatenation of the identity type. We call this the fundamental pregroupoid of XX. It is univalent if and only if XX is a 1-type; its Rezk completion is the fundamental (univalent) groupoid of XX.

  • There is a precategory whose type of objects is the type universe 𝒰\mathcal{U} and with hom(X,Y)≡‖X→Y‖ 0hom(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).

Properties

Theorem

Given two categories AA and BB, if BB is univalent, then the functor category B AB^A is univalent.

Proof

Let F:A→BF:A \to B and G:A→BG:A \to B be functors from AA to BB.

Suppose that γ:F→G\gamma:F \to G is a natural isomorphism. Then for any object a:Ob(A)a : Ob(A), there is an isomorphism γ a:F ob(a)≅G ob(a)\gamma_a: F_{ob}(a) \cong G_{ob}(a) in BB. Since BB is univalent, this shows that F ob(a)=G ob(a)F_{ob}(a) = G_{ob}(a) for all objects aa, and by function extensionality, that F ob=G obF_{ob} = G_{ob}.

Now, for any a:Ob(A)a : Ob(A) and b:Ob(B)b : Ob(B), the functions F mor(a,b):Mor A(a,b)→Mor B(F ob(a),F ob(b))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)→Mor B(G ob(a),G ob(b))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)F(a) = G(a) for all a:Ob(a)a : Ob(a). Because the object functions and morphism functions of FF and GG are equal to each other, F=GF = G.

Thus, if there is an isomorphism γ:F≅G\gamma:F \cong G, then F=GF = G.

this proof needs to be revised since it is missing the explicit identifications

An equivalent-on-objects functor between two precategories AA and BB is a functor F:A→BF:A \to B where the object function F ob:Ob(A)→Ob(B)F_{ob}:Ob(A) \to Ob(B) is a equivalence of types.

A split essentially surjective functor between AA and BB is a functor F:A→BF:A \to B where for every object b:Ob(B)b : Ob(B), there is a specified object a:Ob(A)a : Ob(A) and an isomorphism f:F ob(a)≅bf:F_{ob}(a) \cong b.

A fully faithful functor is a functor F:A→BF:A\to B such that each map on hom-sets F a,b:A(a 0,a 1)→B(F(a 0),F(a 1))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→BF:A \to B which has a left adjoint G:B→AG:B \to A such that the unit η:1 A→GF\eta:1_A \to G F and counit ϵ:FG→1 B\epsilon:F G \to 1_B are isomorphisms.

Theorem

For univalent categories, isomorphism of categories and equivalence of categories coincide.

…

Lemma

In a univalent category, the type of objects is a 1-type.

Proof

It suffices to show that for any a,b:Aa,b:A, the type a=ba=b is a set. But a=ba=b is equivalent to a≅ba \cong b which is a set.

There is a canonical way to turn a category into a univalent category via the Rezk completion.

References

General

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:

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

Formalization of bicategories:

Lemmas and proofs above are taken from:

On monoidal univalent categories:

By coinduction

A formalization in HoTT-Agda of general (n,r)-categories for n,r∈ℕ⊔{∞}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 March 12, 2024 at 04:09:12. See the history of this page for a list of all contributions to it.