nLab univalent category

Redirected from "internal category in homotopy type theory".
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

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming 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 aba\cong b for the type of isomorphisms from aa to bb.

Lemma

There is a map

idtoiso:(a=b)(ab)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)(ab)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”.

Remark

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.

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)(AB)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 0x=y 0y=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)XY 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:ABF:A \to B and G:ABG:A \to B be functors from AA to BB.

Suppose that γ:FG\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 γ:FG\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:ABF: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:ABF: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:ABF: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:ABF:A \to B which has a left adjoint G:BAG:B \to A such that the unit η:1 AGF\eta:1_A \to G F and counit ϵ:FG1 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 aba \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.