The n-Category Café

Setting the Stage

Any “Univalence Principle” type of result has the following form:

$$\forall M, N \in Structures(\mathcal{L}), (M \simeq_\mathcal{L} N) \simeq (M = N)$$

The result gains in strength if the class of $Structures(\mathcal{L})$ is as large as possible, and the notion of equivalence $M \simeq_{\mathcal{L}} N$ between them coincides with known notions of equivalence in practice (where $\mathcal{L}$ is a placeholder for a notion of signature in terms of which $M$ and $N$ are structures). Such a result also gains in strength if the middle notion of equivalence is as “structural” as possible, ensuring that not only properties of the structures are preserved, but also constructions built on top of them. This last feature can only really be pursued within a univalent type theory, like HoTT.

In our work, we define: diagrammatic signatures $\mathcal{L}$ as inverse categories of finite height, $\mathcal{L}$-structures as Reedy-fibrant functors $\mathcal{L} \to \mathcal{U}$, and a notion of indiscernibility relating objects within structures, which yields a derived notion of equivalence $\simeq_{\mathcal{L}}$ between structures (essentially structure-preserving bijections up to indiscernibility). The primitive notions $\simeq$ and $=$ are given by equivalence and equality in 2LTT, appropriately defined.

Signatures, Structures (and where they live)

Two-level type theory (2LTT)

In 2LTT, there is an external level for exo-types and other exo-gizmos (allowing strictly functorial constructions), and the usual fibrant (HoTT/UF) level where mathematical objects live. The external level is the metamathematical or syntactic level, where a strict equality exists that allows us to define syntax and symbols. Our exo-gizmos are analogous to sets of syntactical symbols used to define signatures in first-order logic.

Such syntax consists of categories with strict equality on composition, which we call exo-categories. Equalities here are strict (exo-equalities), while the internal world has homotopical paths. The 2LTT setting is convenient for type-theoretic reasoning, and allows us to neatly separate the various notions of equality at play.

Diagram signatures are inverse categories of finite height

A diagram signature $\mathcal{L}$ is an inverse exo-category of finite height equipped with a rank functor $$\mathrm{rk}:\mathcal{L} \longrightarrow (\mathbb{N}^{\mathrm{exo}})^{\mathrm{op}}$$ that reflects identities. Objects of $\mathcal{L}$ are the sorts (analogous to “sorts” in first-order logic); morphisms encode dependencies (“an arrow depends on a pair of objects,” etc.). Inverse-ness gives matching objects and allows Reedy methods to apply.

To illustrate the idea, take the example of a reflexive graph. The diagram signature for reflexive graphs would be given by the following inverse (exo-)category

$$\array{ I \\ \downarrow^i \\ A \\ \downarrow_{c} \;\; \downarrow_{d} \\ O }$$

where $c i = d i$. The intuition is that we have a sort $A$ of “arrows” between any two objects, and a predicate $I$ (“identity”) that can be used to select which arrows are identity arrows with the relation ensuring that this predicate can only be “asked” of loops.

Structures are Reedy fibrant diagrams over these signatures

Given this notion of a signature, a structure in our sense is simply a (Reedy fibrant) functor $\mathcal{L} \to \mathcal{U}$. In more detail, a raw $\mathcal{L}$-diagram is an exo-functor $$M:\mathcal{L}\to\mathcal{U}^{\mathrm{exo}}$$ For each sort $K$, the matching object $\mathbb{M}_{K}M$ collects the compatible lower-rank data needed to specify the “boundary” for an element of $M K$. The Reedy fibrancy condition is: the canonical boundary map $M_K\to \mathbb{M}_{K}M$ is a fibration (i.e., a dependent type) for each $K$. The category of such Reedy-fibrant diagrams then forms a fibrant type $\mathrm{Str}(\mathcal{L})$ whose points are the $\mathcal{L}$-structures.

To illustrate with the example of $\mathcal{L}_{rg}$ from above, an $\mathcal{L}_{rg}$-structure $G$ in our sense would be given by the following data, in type-theoretic notation:

• A type $GO:\mathcal{U}$
• A family $GA: GO\times GO\to\mathcal{U}$ dependent on $GO$
• A family $GI:\prod_x GA(x,x)\to\mathcal{U}$ for the “identity”

The trick here is to ensure the repeated $x$ in the definition of $GI$, obeying the relations of the signature. This is what the matching object machinery achieves for arbitrary signatures.

Other examples of $\mathcal{L}$-structures include: categories (with sorts for objects and morphisms), groupoids, $n$-categories for any $n$, preorders, and models of higher-order theories like topological spaces and sup-lattices. Furthermore, all of what we say applies to theories with axioms (not just structures), which we define in the book too.

Indiscernibility and local univalence

With our formal set-up complete, we address the central question: for arbitrary signatures $\mathcal{L}$, when are two “objects” in an $\mathcal{L}$-structure equivalent? Such an “object” could be a categorical (or higher-categorical) gadget itself when $\mathcal{L}$ has height $\gt 2$, e.g. the “objects” of $\mathbf{2-}\mathbf{Cat}$ are themselves categories, which are $\mathcal{L}'$-structures for an $\mathcal{L}'$ of lower height. The key idea is: two “objects” are indiscernible if nothing in the signature can distinguish them…up to indiscernibility!

Indiscernibilities and Local Univalence

Fix a signature $\mathcal{L}$, an $\mathcal{L}$-structure $M$, a rank $0$ (“bottom”) sort $K: \mathcal{L}(0)$, and elements $a,b:M K$. Think of $K$ as a “set” of objects (e.g. of a category) on top of which properties and structures are defined.

To define when $a$ and $b$ are indiscernible, we package together everything that could distinguish them. The intuition is: if there is an equivalence between “everything you can say about $a$” and “everything you can say about $b$” (outside of directly referencing $a$ or $b$ themselves), then they are indiscernible. We achieve this through a formal definition of a “boundary” $\partial_a M$, which one can think of as the $\mathcal{L}$-structure that contains everything that could distinguish $a$ in $MK$ from anything else in $MK$. Which naturally leads us to the following definitions.

Definition (Indiscernibility). We say that $a,b : MK$ are indisernible, written $a\approx b$, iff there is a levelwise equivalence $\partial_a M \simeq \partial_b M$ that is coherent in the right way.

Definition (Univalent Structure). We say that $M$ is locally univalent at K if the canonical map $$(a=b) \;\longrightarrow\; (a\approx b)$$ is an equivalence. We then say a structure $M$ is univalent if this holds at all rank-0 sorts and (recursively) for all sorts of higher rank.

We prove our main results for univalent $\mathcal{L}$-structures. These are quite special in that they are “saturated” in their equivalence information: two indistinguishable gizmos are actually equal. Or, put differently: when there is not “enough” structure to distinguish two gizmos, there is always enough to prove them equivalent. Some examples to illustrate (see Part 2 of the book for many more!):

• In a reflexive graph structure, two nodes $a$ and $b$ are indiscernible iff they have the same number of arrows coming in and out, and the same number of loops that are identities.
• In a category, two objects are indiscernible iff they are isomorphic. A univalent category is precisely a category (precategory in UF) that is locally univalent at the sort of its objects.
• In an appropriately defined bicategory, an indiscernibility amounts to a pair of coherent adjoint equivalenes, as expected.

Equivalences of structures

We are almost there! On to the final missing piece: equivalences between structures themselves. Let $f:M\to N$ be a morphism of $\mathcal{L}$-structures, defined in the expected way (as a natural transformation between the corresponding $\mathcal{U}$-valued functors). Then, for each sort $K$, we have a matching square

$$\array{ MK & \overset{\rightarrow}{f_K} & NK\\ \downarrow & & \downarrow \\ \mathbb{M}_KM & \overset{\rightarrow}{\mathbb{M}_K f} & \mathbb{N}_KN }$$

and for each “context” $z: \mathbb{M}_KM$ an induced fiber map $$f_{K,z}: (MK)_z \longrightarrow (NK)_{\,\mathbb{M}_K f(z)}.$$ Write $\approx$ for indiscernibility at sort $K$ (as above). Then, what we really want to say now is: $M$, $N$ are equivalent if they are “level-wise equivalent up to indiscernibility”. This idea gives us the $\simeq_{\mathcal{L}}$ from the beginning, and we define it as follows:

Definition (Equivalence of $\mathcal{L}$-structures). $f$ is an equivalence if, for every sort $K$, every $z : \mathbb{M}_KM$, and every $y : (N_K)_{\mathbb{M}_K f(z)}$, there exists a specified $x : (MK)_z$ with $$f_{K,z}(x)\;\approx\; y$$ i.e., $f_{K,z}$ is essentially split surjective up to indiscernibility on each fiber. We write $M \simeq_{\mathcal{L}} N$ for the type of equivalences.

The key innovation is the “up to indiscernibility” part; it makes our notion significantly weaker than usual notions, and hence the final result stronger. Note that we have not been able to prove our result without a splitness condition in the definition of equivalence, and to our mind this remains an open problem.

Our definition is related to Makkai’s original notion of FOLDS equivalence, but Makkai was not able to define a general notion of non-surjective equivalence directly, relying instead on spans. Our notion of indiscernibility circumvents this difficulty and allows us to consider the whole structure of equivalences between structures.

The Univalence Principle

With all our apparatus in place we prove our main result, a very general form of a univalence principle, as promised.

Theorem (“The Univalence Principle”). For a signature $\mathcal{L}$ and univalent $\mathcal{L}$-structures $M,N$, the canonical map $$(M = N) \;\longrightarrow\; (M \simeq_{\mathcal{L}} N)$$ is an equivalence of types. In other words, $(M = N) \simeq (M \simeq_{\mathcal{L}} N)$.

The proof proceeds by induction on the height of $\mathcal{L}$. The key insight is that level-wise equivalences between univalent structures must “reflect indiscernibilities”: if $f$ doesn’t preserve the ability to distinguish elements, then whatever structure distinguishes them in the source would transfer to structure distinguishing their images in the target, contradicting the equivalence. With the splitness assumption in the map and the assumption of univalence (of our $\mathcal{L}$-structure), we are able to achieve the lifting of the indiscernibility.

Our result is actually proved for an even more general class of signatures called functorial signatures, which strictly extends diagram signatures and covers “higher-order” situations (topological spaces, suplattices, DCPOs, etc.). We have stuck to the diagrammatic view in this post for intuition, but all results and definitions carry over to this more general notion.

Conclusion

In the course of this work there were quite a few questions we tried to answer, but could not. To mention a couple: Can we define a Rezk completion for arbitrary structures, providing a universal way to turn any structure into a univalent one? Can we remove the splitness condition from our definition of equivalence between structures? We list more open problems at the end of the book.

Beyond our specific result, the framework in which it is proven establishes a way to answer metamathematical questions around the univalence axiom in a precise and fruitful way. It is important to emphasize that carrying out this type of mathematical study does not require choosing one foundation over the other. In any setting that interprets the fibrant part of 2LTT, the univalence principle will hold, including in set theory.

The metamathematics of UF is the mathematical study of formalizing mathematics in terms of a hierarchy of $h$-levels vs. a cumulative hierarchy of sets. Formalizing mathematics in this way has all sorts of unique mathematical properties. The Univalence Principle is one of them.