Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 24, 2017

A Type Theory for Synthetic ∞-Categories

Posted by Emily Riehl

One of the observations that launched homotopy type theory is that the rule of identity-elimination in Martin-Löf’s identity types automatically generates the structure of an \infty-groupoid. In this way, homotopy type theory can be viewed as a “synthetic theory of \infty-groupoids.”

It is natural to ask whether there is a similar directed type theory that describes a “synthetic theory of (,1)(\infty,1)-categories” (or even higher categories). Interpreting types directly as (higher) categories runs into various problems, such as the fact that not all maps between categories are exponentiable (so that not all \prod-types exist), and that there are numerous different kinds of “fibrations” given the various possible functorialities and dimensions of categories appearing as fibers. The 2-dimensional directed type theory of Licata and Harper has semantics in 1-categories, with a syntax that distinguishes between co- and contra-variant dependencies; but since the 1-categorical structure is “put in by hand”, it’s not especially synthetic and doesn’t generalize well to higher categories.

An alternative approach was independently suggested by Mike and by Joyal, motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the \infty-cosmos of complete Segal spaces, which we call Rezk spaces. It is not possible to model ordinary homotopy type theory directly in the Rezk model structure, which is not right proper, but we can model it in the Reedy model structure and then identify internally some “types with composition,” which correspond to Segal spaces, and “types with composition and univalence,” which correspond to the Rezk spaces.

Almost five years later, we are finally developing this approach in more detail. In a new paper now available on the arXiv, Mike and I give definitions of Segal and Rezk types motivated by these semantics, and demonstrate that these simple definitions suffice to develop the synthetic theory of (,1)(\infty,1)-categories. So far this includes functors, natural transformations, co- and contravariant type families with discrete fibers (\infty-groupoids), the Yoneda lemma (including a “dependent” Yoneda lemma that looks like “directed identity-elimination”), and the theory of coherent adjunctions.

Cofibrations and extension types

One of the reasons this took so long to happen is that it required a technical innovation to become feasible. To develop the synthetic theory of Segal and Rezk types, we need to detect the semantic structure of the simplicial spaces model internally, and it seems that the best way to do this is to axiomatize the presence of a strict interval 22 (a totally ordered set with distinct top and bottom elements). This is the geometric theory of which simplicial sets are the classifying topos (and of which simplicial spaces are the classifying (,1)(\infty,1)-topos). We can then define an arrow in a type AA to be a function 2A2\to A.

However, often we want to talk about arrows with specified source and target. We can of course define the type hom A(x,y)\hom_A(x,y) of such arrows to be f:2A(f(0)=x)×(f(1)=y)\sum_{f:2\to A} (f(0)=x)\times (f(1)=y), but since we are in homotopy type theory, the equalities f0=xf0=x and f1=yf1=y are data, i.e. homotopical paths, that have to be carried around everywhere. When we start talking about 2-simplices and 3-simplices with specified boundaries as well, the complexity becomes unmanageable.

The innovation that solves this problem is to introduce a notion of cofibration in type theory, with a corresponding type of extensions. If i:ABi:A\to B is a cofibration and X:B𝒰X:B\to \mathcal{U} is a type family dependent on BB, while f: a:AX(i(a))f:\prod_{a:A} X(i(a)) is a section of XX over ii, then we introduce an extension type b:BX(b) f i\langle \prod_{b:B} X(b) \mid^i_f\rangle consisting of “those dependent functions g: b:BX(b)g:\prod_{b:B} X(b) such that g(i(a))f(a)g(i(a)) \equiv f(a) — note the strict judgmental equality! — for any a:Aa:A”. This is modeled semantically by a “Leibniz” or “pullback-corner” map. In particular, we can define hom A(x,y)= t:2A [x,y] 0,1\hom_A(x,y) = \langle \prod_{t:2} A \mid^{0,1}_{[x,y]} \rangle, the type of functions f:2Af:2\to A such that f(0)xf(0)\equiv x and f(1)yf(1) \equiv y strictly, and so on for higher simplices.

General extension types along cofibrations were first considered by Mike and Peter Lumsdaine for a different purpose. In addition to the pullback-corner semantics, they are inspired by the path-types of cubical type theory, which replace the inductively specified identity types of ordinary homotopy type theory with a similar sort of restricted function-type out of the cubical interval. Our paper introduces a general notion of “type theory with shapes” and extension types that includes the basic setup of cubical type theory as well as our simplicial type theory, along with potential generalizations to Joyal’s “disks” for a synthetic theory of (,n)(\infty,n)-categories.

Simplices in the theory of a strict interval

In simplicial type theory, the cofibrations are the “inclusions of shapes” generated by the coherent theory of a strict interval, which is axiomatized by the interval 22, top and bottom elements 0,1:20,1 : 2, and an inequality relation \le satisfying the strict interval axioms.

Simplices can then be defined as

Δ n:={t 1,,t nt nt n1t 2t 1} \Delta^n := \{ \langle t_1,\ldots, t_n\rangle \mid t_n \leq t_{n-1} \cdots t_2 \leq t_1 \}

Note that the 1-simplex Δ 1\Delta^1 agrees with the interval 22.

Boundaries, e.g. of the 2-simplex, can be defined similarly Δ 2:={t 1,t 2:2×2(0t 2t 1)(t 2t 1)(t 2t 11)} \partial\Delta^2 :=\{⟨t_1,t_2⟩: 2 \times 2 \mid (0 \equiv t_2 \leq t_1) \vee (t_2 \equiv t_1) \vee (t_2 \leq t_1 \equiv 1)\} making the inclusion of the boundary of a 2-simplex into a cofibration.

Segal types

For any type AA with terms x,y:Ax,y : A define

hom A(x,y):=2A [x,y] Δ 1 hom_A(x,y) := \langle 2 \to A \mid^{\partial\Delta^1}_{ [x,y]} \rangle

That is, a term f:hom A(x,y)f : hom_A(x,y), which we call an arrow from xx to yy in AA, is a function f:2Af: 2 \to A so that f(0)xf(0) \equiv x and f(1)yf(1) \equiv y. For f:hom A(x,y)f : hom_A(x,y), g:hom A(y,z)g : hom_A(y,z), and h:hom A(x,z)h : hom_A(x,z), a similar extension type

hom A(x,y,z,f,g,h):=Δ 2A [x,y,z,f,g,h] Δ 2 hom_A(x,y,z,f,g,h) := \langle \Delta^2 \to A \mid^{\partial\Delta^2}_{[x,y,z,f,g,h]}\rangle

has terms that we interpret as witnesses that hh is the composite of ff and gg. We define a Segal type to be a type in which any composable pair of arrows admits a unique (composite, witness) pair. In homotopy type theory, this may be expressed by saying that AA is Segal if and only if for all f:hom A(x,y)f : hom_A(x,y) and g:hom A(y,z)g : hom_A(y,z) the type

h:hom A(x,z)hom A(x,y,z,f,g,h) \sum_{h : hom_A(x,z)} hom_A(x,y,z,f,g,h)

is contractible. A contractible type is in particular inhabited, and an inhabitant in this case defines a term gf:hom A(x,z)g \circ f : hom_A(x,z) that we refer to as the composite of ff and gg, together with a 2-simplex witness comp(g,f):hom A(x,y,z,f,g,gf)comp(g,f) : hom_A(x,y,z,f,g,g \circ f).

Somewhat surprisingly, this single contractibility condition characterizing Segal types in fact ensures coherent categorical structure at all dimensions. The reason is that if AA is Segal, then the type XAX \to A is also Segal for any type or shape XX. For instance, applying this result in the case X=2X=2 allows us to prove that the composition operation in any Segal type is associative. In an appendix we prove a conjecture of Joyal that in the simplical spaces model this condition really does characterize exactly the Segal spaces, as usually defined.

Discrete types

An example of a Segal type is a discrete type, which is one for which the map

idtoarr: x,y:A(x= Ay)hom A(x,y) idtoarr : \prod_{x,y: A} (x=_A y) \to hom_A(x,y)

defined by identity elimination by sending the reflexivity term to the identity arrow, is an equivalence. In a discrete type, the \infty-groupoid structure encoded by the identity types and equivalent to the (,1)(\infty,1)-category structure encoded by the hom types. More precisely, a type AA is discrete if and only if it is Segal, as well as Rezk-complete (in the sense to be defined later on), and moreover “every arrow is an isomorphism”.

The dependent Yoneda lemma

If AA and BB are Segal types, then any function f:ABf:A\to B is automatically a “functor”, since by composition it preserves 2-simplices and hence witnesses of composition. However, not every type family C:A𝒰C:A\to \mathcal{U} is necessarily functorial; in particular, the universe 𝒰\mathcal{U} is not Segal — its hom-types hom 𝒰(X,Y)\hom_{\mathcal{U}}(X,Y) consist intuitively of “spans and higher spans”. We say that C:A𝒰C:A\to \mathcal{U} is covariant if for any f:hom A(x,y)f:\hom_A(x,y) and u:C(x)u:C(x), the type

v:C(y) t:2C(f(t)) [u,v] Δ 1 \sum_{v:C(y)} \langle \prod_{t:2} C(f(t)) \mid^{\partial\Delta^1}_{[u,v]}\rangle

of “liftings of ff starting at uu” is contractible. An inhabitant of this type consists of a point f *(u):C(y)f_\ast(u):C(y), which we call the (covariant) transport of uu along ff, along with a witness trans(f,u)trans(f,u). As with Segal types, this single contractibility condition suffices to ensure that this action is coherently functorial. It also ensures that the fibers C(x)C(x) are discrete, and that the total space x:AC(x)\sum_{x:A} C(x) is Segal.

In particular, for any Segal type AA and any a:Aa:A, the hom-functor hom A(a,):A𝒰\hom_A(a,-) :A \to \mathcal{U} is covariant. The Yoneda lemma says that for any covariant C:A𝒰C:A\to \mathcal{U}, evaluation at (a,id a)(a,id_a) defines an equivalence

( x:Ahom A(a,x)C(x))C(a) \Big(\prod_{x:A} \hom_A(a,x) \to C(x)\Big) \simeq C(a)

The usual proof of the Yoneda lemma applies, except that it’s simpler since we don’t need to check naturality or functoriality; in the “synthetic” world all of that comes for free.

More generally, we have a dependent Yoneda lemma, which says that for any covariant C:( x:Ahom A(a,x))𝒰C : \Big(\sum_{x:A} \hom_A(a,x)\Big) \to \mathcal{U}, we have a similar equivalence

( x:A f:hom A(a,x)C(x,f))C(a,id a). \Big(\prod_{x:A} \prod_{f:\hom_A(a,x)} C(x,f)\Big) \simeq C(a,id_a).

This should be compared with the universal property of identity-elimination (path induction) in ordinary homotopy type theory, which says that for any type family C:( x:A(a=x))𝒰C : \Big(\sum_{x:A} (a=x)\Big) \to \mathcal{U}, evaluation at (a,refl a)(a,refl_a) defines an equivalence

( x:A f:a=xC(x,f))C(a,refl a). \Big(\prod_{x:A} \prod_{f:a=x} C(x,f)\Big) \simeq C(a,refl_a).

In other words, the dependent Yoneda lemma really is a “directed” generalization of path induction.

Rezk types

When is an arrow f:hom A(x,y)f : hom_A(x,y) in a Segal type an isomorphism? Classically, ff is an isomorphism just when it has a two-sided inverse, but in homotopy type theory more care is needed, for the same reason that we have to be careful when defining what it means for a function to be an equivalence: we want the notion of “being an isomorphism” to be a mere proposition. We could use analogues of any of the equivalent notions of equivalence in Chapter 4 of the HoTT Book, but the simplest is the following:

isiso(f):=( g:hom A(y,x)gf=id x)×( h:hom A(y,x)fh=id y) isiso(f) := \left(\sum_{g : hom_A(y,x)} g \circ f = id_x\right) \times \left(\sum_{h : hom_A(y,x)} f \circ h = id_y \right)

An element of this type consists of a left inverse and a right inverse together with witnesses that the respective composites with ff define identities. It is easy to prove that g=hg = h, so that ff is an isomorphism if and only if it admits a two-sided inverse, but the point is that any pair of terms in the type isiso(f)isiso(f) are equal (i.e., isiso(f)isiso(f) is a mere proposition), which would not be the case for the more naive definition.

The type of isomorphisms from xx to yy in AA is then defined to be

(x Ay):= f:hom A(x,y)isiso(f). (x \cong_A y) := \sum_{f : \hom_A(x,y)} isiso(f).

Identity arrows are in particular isomorphisms, so by identity-elimination there is a map

x,y:A(x= Ay)(x Ay) \prod_{x,y: A} (x =_A y) \to (x \cong_A y)

and we say that a Segal type AA is Rezk complete if this map is an equivalence, in which case AA is a Rezk type.

Coherent adjunctions

Similarly, it is somewhat delicate to define homotopy correct types of adjunction data that are contractible when they are inhabited. In the final section to our paper, we compare transposing adjunctions, by which we mean functors f:ABf : A \to B and u:BAu : B \to A (i.e. functions between Segal types) together with a fiberwise equivalence

a:A,b:Bhom A(a,ub)hom B(fa,b) \prod_{a :A, b: B} \hom_A(a,u b) \simeq \hom_B(f a,b)

with various notions of diagrammatic adjunctions, specified in terms of units and counits and higher coherence data.

The simplest of these, which we refer to as a quasi-diagrammatic adjunction is specified by a pair of functors as above, natural transformations η:Id Auf\eta: Id_A \to u f and ϵ:fuId B\epsilon : f u \to Id_B (a “natural transformation” is just an arrow in a function-type between Segal types), and witnesses α\alpha and β\beta to both of the triangle identities. The incoherence of this type of data has been observed in bicategory theory (it is not cofibrant as a 2-category) and in (,1)(\infty,1)-catgory theory (as a subcomputad of the free homotopy coherent adjunction it is not parental). One homotopically correct type of adjunction data is a half-adjoint diagrammatic adjunction, which has additionally a witness that fα:ϵfuϵfηuϵf \alpha : \epsilon \circ f u\epsilon \circ f\eta u \to \epsilon and βu:ϵϵfufηu\beta u: \epsilon \circ \epsilon f u \circ f \eta u commute with the naturality isomorphism for ϵ\epsilon.

We prove that given Segal types AA and BB and functors f:ABf : A \to B and u:BAu : B \to A, the type of half-adjoint diagrammatic adjunctions between them is equivalent to the type of transposing adjunctions. More precisely, if in the notion of transposing adjunction we interpret “equivalence” as a “half-adjoint equivalence”, i.e. a pair of maps ϕ\phi and ψ\psi with homotopies ϕψ=1\phi \psi = 1 and ψϕ=1\psi \phi = 1 and a witness to one of the triangle identities for an adjoint equivalence (this is another of the coherent notions of equivalence from the HoTT Book), then these data correspond exactly under the Yoneda lemma to those of a half-adjoint diagrammatic adjunction.

This suggests that similar correspondences for other kinds of coherent equivalences. For instance, if we interpret transposing adjunctions using the “bi-invertibility” notion of coherent equivalence (specification of a separate left and right inverse, as we used above to define isomorphisms in a Segal type), we obtain upon Yoneda-fication a new notion of coherent diagrammatic adjunction, consisting of a unit η\eta and two counits ϵ,ϵ\epsilon,\epsilon', together with witnesses that η,ϵ\eta,\epsilon satisfy one triangle identity and η,ϵ\eta,\epsilon' satisfy the other triangle identity.

Finally, if the types AA and BB are not just Segal but Rezk, we can show that adjoints are literally unique, not just “unique up to isomorphism”. That is, given a functor u:BAu:B\to A between Rezk types, the “type of left adjoints to uu” is a mere proposition.

Posted at May 24, 2017 12:11 AM UTC

TrackBack URL for this Entry:

13 Comments & 0 Trackbacks

Re: A Type Theory for Synthetic ∞-Categories

“… the path-types of cubical type theory, …”

has a bogus link which should be

Posted by: RodMcGuire on May 24, 2017 4:43 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

Thanks, fixed.

Posted by: Emily Riehl on May 25, 2017 6:05 AM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories


Posted by: Jack Morava on May 24, 2017 11:13 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

By the way, we did some of the work on this project on the weekend of the Mid-Atlantic Topology Conference. The supporting NSF conference grant is mentioned in the paper’s acknowledgments.

Posted by: Emily Riehl on May 25, 2017 1:30 AM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

What is the relation between Segal/Rezk types and precategories/univalent categories?

Is it true (in the type theory) that the type of all Segal/Rezk types with hom-types that are h-sets is equivalent to the type of precategories/univalent categories as usually defined?

Posted by: Dimitris on May 25, 2017 3:18 AM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

There is some analogy Segal : Rezk :: precategory : univalent category. However, Segal/Rezk types are synthetic, meaning they are basic objects of the theory, whereas precategories and univalent categories are structures constructed in the theory (and, generally, in a theory whose basic objects are considered as \infty-groupoids rather than \infty-category-like structures).

One thing that should be true is that Segal and Rezk types whose homs are sets, when interpreted semantically in the bisimplicial spaces model, yield notions that are equivalent to precategories and univalent categories, respectively, when the latter are interpreted semantically in the ordinary spaces model. Does that help clarify?

Posted by: Mike Shulman on May 25, 2017 4:05 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

I’m not sure. Emily writes:

We define a Segal type to be a type in which any composable pair of arrows admits a unique (composite, witness) pair. In homotopy type theory, this may be expressed by saying that AA is Segal if and only if for all f:hom A(x,y)f : hom_A(x,y) and g:hom A(y,z)g \colon hom_A(y,z) the type h:hom A(x,z)hom A(x,y,z,f,g,h) \sum_{h : hom_A(x,z)} hom_A(x,y,z,f,g,h) is contractible.

How am I to understand this other than that Segal types are types satisfying certain properties expressed in terms of the (new, synthetic) homhom-types?

In particular, can I not define the type of Segal types whose hom-types are hh-sets? This is a constructed object (to use your terminology) that can be compared to another constructed object e.g. to precategories as traditionally defined.

Similarly for Rezk types.

Posted by: Dimitris on May 25, 2017 4:44 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

I suppose for the case of Rezk types what I am asking is the analogue of the question of the relationship between the type Gpd UGpd_U of 1-types and the type of “univalent groupoids”, i.e. of univalent categories all of whose arrows are isomorphisms. In “Book HoTT” these two types are equivalent, I think.

For Segal types the analogous question would probably be the relationship between (general) types and pregroupoids, i.e. precategories that are groupoids with respect to the category structure, of which there is no interesting relation as far as I can tell.

Posted by: Dimitris on May 25, 2017 7:14 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

the analogue of the question of the [equivalence] between the type Gpd UGpd_U of 1-types and the type of “univalent groupoids”.

Okay, here is an analogue of that. Consider a precategory AA, which has a type A 0A_0 and hom-sets Mor A:A 0A 0Type 0Mor_A : A_0 \to A_0 \to Type_0, with composition and so on. A priori there is no relationship between Mor AMor_A and hom A\hom_A. They even take values in different places: Mor AMor_A lands in 0-types (that may not be discrete) while hom A\hom_A lands in discrete types (that may not be truncated).

Now suppose as an additional axiom that Mor AMor_A is a “two-sided discrete fibration”, i.e. it is contravariant in its first argument and covariant in its second. This implies that it takes discrete values. Now the precategory identities idmor: x:A 0Mor A(x,x)idmor : \prod_{x:A_0} Mor_A(x,x) induce, by the Yoneda lemma, a family of maps arrtomor: x,y:A 0hom A(x,y)Mor A(x,y)arrtomor : \prod_{x,y:A_0} \hom_A(x,y) \to Mor_A(x,y) such that arrtomor(id x)=idmor xarrtomor(id_x) = idmor_x. This is a directed analogue of the map idtoisoidtoiso for a precategory. Define AA to be univalent if each arrtomor x,yarrtomor_{x,y} is an equivalence (and therefore, in particular, each hom A(x,y)\hom_A(x,y) is a 0-type).

I would expect that Segal types such that hom\hom lands in 0-types are equivalent to precategories that are two-sided discrete fibrations and univalent in this sense.

Posted by: Mike Shulman on May 25, 2017 7:42 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

Nice. Thanks a lot.

Posted by: Dimitris on May 26, 2017 7:48 PM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

A fruitful 2017 for Mike so far! That’s 5 papers on the arXiv and a sixth here.

Posted by: David Corfield on May 28, 2017 9:16 AM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

I’m bemused by the Rezk type gizmo and its relation to univalence. I’d think UA was asserting the universe is Rezk complete, yet Rezk completion is stated as a property of Segal types (of which I’m unsure if the universe is).

Posted by: Jacob A. Gross on May 29, 2017 3:16 AM | Permalink | Reply to this

Re: A Type Theory for Synthetic ∞-Categories

Maybe it’ll help to step back a bit.

If we start from set theory, and define higher categories directly in terms of sets (so that we have exactly one set of nn-morphisms for all nn), then the Rezk condition doesn’t make sense. (Well, technically you can write it down, but the result isn’t something you would want to impose as part of a definition of higher category.) For example, this applies to quasicategories as a definition of (,1)(\infty,1)-category.

The Rezk condition first arises when we start from \infty-groupoid theory, and define other higher categories in terms of those. Here by “\infty-groupoid theory” I mean either an “analytic” theory of \infty-groupoids that are themselves defined in terms of sets, such as simplicial sets with the Kan-Quillen model structure, or a “synthetic” theory of \infty-groupoids such as ordinary (or cubical) homotopy type theory. The point is just that we start with some “notion of \infty-groupoid” and then define an (,1)(\infty,1)-category to be of a bunch of \infty-groupoids with some operations relating them.

Perhaps the most straightforward naive way to define an (,1)(\infty,1)-category-like-structure in terms of \infty-groupoids is as a Segal space: a simplicial diagram of \infty-groupoids such that X nX 1× X 0× X 0X 1X_n \to X_1 \times_{X_0} \cdots \times_{X_0} X_1 is an equivalence. This gives all the correct algebraic structure of an (,1)(\infty,1)-category, but it has “too much data”, because the \infty-groupoids X nX_n have their own higher structure. A kk-cell in X nX_n represents a sort of “(n+k)(n+k)-cell” in XX, but if n+k=n+kn'+k'=n+k then the kk'-cells in X nX_{n'} need not be equivalent to the kk-cells in X nX_n. The Rezk condition collapses all this extra information by forcing all of these different kinds of cells of the same dimension to indeed be equivalent — at least insofar as it makes sense, because for instance a 00-cell in X 1X_1 and a 11-cell in X 0X_0 are both a sort of 1-cell in XX, but the first need not be invertible while the second always must be. So we only require that the 1-cells in X 0X_0 are equivalent to those 0-cells in X 1X_1 that happen to be invertible. This gives a correct definition of “(,1)(\infty,1)-category” in terms of our original theory of \infty-groupoids.

Now inside our theory of \infty-groupoids, we might have some “universe”, i.e. an “\infty-groupoid of \infty-groupoids”. Using the local cartesian closure of our theory of \infty-groupoids, we can then construct a Segal space UU where U 0U_0 is that universe, and where the 0-cells in U 1U_1 are, by definition, the “morphisms” in our theory of \infty-groupoids. This is an \infty-categorical version of what in 1-topos theory is called an “internal full subcategory”. The univalence axiom for our theory of \infty-groupoids asserts that this Segal space UU is in fact Rezk-complete. (For \infty-groupoids defined in terms of sets, this “axiom” is provable; for ordinary homotopy type theory it is an axiom we have to assert; for cubical homotopy type theory it is once again provable.)

The next step is to ask what happens if we start from a theory of (,1)(\infty,1)-categories: either an analytic one defined in terms of sets, or an as-yet-unspecified synthetic one. (Don’t think about our paper yet, just imagine a hypothetical theory in which all objects are (,1)(\infty,1)-categories, or an unspecified set-theoretic model such as infinity-cosmoi .) Here there is no need for a Segal or Rezk condition: those were used in order to define (,1)(\infty,1)-categories in terms of \infty-groupoids, but in this case all the objects of our theory are already (,1)(\infty,1)-categories.

In particular, in a theory of (,1)(\infty,1)-categories we might have many different universes. For instance, there should be an (,1)(\infty,1)-category Gpd\infty Gpd of \infty-groupoids, and also an (,1)(\infty,1)-category (,1)Cat(\infty,1)Cat of (,1)(\infty,1)-categories, as well as their opposites. All of these will be (,1)(\infty,1)-categories just because they are objects of our theory; there is no sense to ask whether they are Segal or Rezk.

Now, the theory that Emily and I are presenting here is neither of the above two things. It has elements of both, but technically what it really is is a synthetic theory of simplicial \infty-groupoids (i.e. simplicial diagrams of \infty-groupoids). That is, the basic objects of the theory (“types”) are “simplicial \infty-groupoids” (at least, in the same sense that the types in ordinary homotopy type theory “are” ordinary \infty-groupoids). Since simplicial \infty-groupoids are an intermediate step in the construction of (,1)(\infty,1)-categories starting from a theory of \infty-groupoids, we can reproduce that same construction by just starting from our “synthetic simplicial \infty-groupoids” rather than building simplicial \infty-groupoids out of ordinary \infty-groupoids. (This is convenient because, among other reasons, we don’t know how to build simplicial \infty-groupoids out of the “ordinary \infty-groupoids” or ordinary homotopy type theory, due to the problem of infinite objects.)

In particular, we have to assert Segal and Rezk conditions to characterize those simplicial \infty-groupoids that “are” (,1)(\infty,1)-categories, just as we did in the first approach. So in this sense our Segal and Rezk types are not really “fully synthetic” (,1)(\infty,1)-categories; their synthetic-ness is extended further but not all the way.

Now as regards univalence, it ought to be possible to extend our theory with various universes. There should be analogues of Gpd\infty Gpd and (,1)Cat(\infty,1)Cat and their opposites, all of which should be Rezk types. But it’s a bit confusing because there is also a native “universe” in the world of simplicial \infty-groupoids. That is, while Gpd\infty Gpd is the (,1)(\infty,1)-category of \infty-groupoids, incarnated (in our theory) as a simplicial \infty-groupoid, this native universe is the simplicial \infty-groupoid of simplicial \infty-groupoids — the object classifier in Gpd Δ op\infty Gpd^{\Delta^{op}}.

This universe is “univalent” in the sense appropriate to a simplicial \infty-groupoid. That is, if we build an internal full subcategory on it in the world of simplicial \infty-groupoids, obtaining a simplicial simplicial \infty-groupoid satisfying the Segal condition, then this Segal object is a Rezk object. This Rezk-ness is in the second simplicial direction, which is not synthetic.

By contrast, in the first simplicial direction, which is synthetic, this universe is not Rezk, and indeed not even Segal. I haven’t worked out exactly what it looks like, but I think it consists roughly of “spans and higher spans”. So while it’s technically useful for working with dependent types in the theory, it doesn’t have a very important meaning when we want to use simplicial \infty-groupoids to talk about (,1)(\infty,1)-categories.

Posted by: Mike Shulman on May 30, 2017 6:29 AM | Permalink | Reply to this

Post a New Comment