# Defining (infinity,1)-categories in HoTT using only an interval type

In this article, Emily Riehl and Michael Shulman describe a type theory in which one can do $$\infty$$-category theory synthetically. Their framework allows them to define simplices $$\Delta^n$$, and a morphism in a type $$A$$ is simply a map $$\Delta^1 \to A$$. Any map $$H: \Delta^2 \to A$$ witnesses its 'bottom edge' $$d_1(H): \Delta^1 \to A$$ as a composite of 'top edges' $$d_2(H)$$ and $$d_0(H)$$. We can then think of the type $$A$$ as a (higher) category if it is a Segal type, which is a type in which every two composable morphisms have a contractible choice of composites.

1. The type theory introduced in the article is a lot more involved than the type theory from the HoTT book. It uses several layers of type theory, using so-called cubes, topes and shapes. To what extent are these extra layers necessary? It would seem to me that one could develop this whole theory in the setting of the HoTT book, with only an additional directed interval type $$\mathbb{I}$$ (some thoughs on this below.) Does this approach make sense? Has it been worked out by someone already? What are the pros/cons for either approach? (Perhaps this is already contained in the recent work on the cubical approach to Homotopy Type Theory, with which, I should say, I am not yet really familiar...)

2. For some types, like the type of groups, we already have a natural notion of morphism around. How can we relate this notion of morphism to the abstract notion of a morphism defined via maps out of $$\Delta^1$$? Does it make sense to add an axiom about the universe $$\mathcal{U}$$ saying that for types $$A,B:\mathcal{U}$$, we have an equivalence $$A \to B \simeq \text{hom}_{\mathcal{U}}(A,B)$$ between the function type $$A \to B$$ and the morphisms in $$\mathcal{U}$$ from $$A$$ to $$B$$? In this case, how do we make sure that maps $$\Delta^2 \to \mathcal{U}$$ actually correspond to (homotopy) commutative diagrams? Once you have both of these things, I think it should follow that for example $$\text{hom}_{Grp}(G,H)$$ is precisely the type of group homomorphisms from $$G$$ to $$H$$ as given in the HoTT book.

Some thoughts on synthetic category theory with just an interval

Let me spell out what I had in mind in point 1. Say that instead of these cubes/topes/shapes we only include an interval type $$\mathbb{I}$$ with constructors $$0,1:\mathbb{I}$$ and $$\lor,\land: \mathbb{I} \to (\mathbb{I} \to \mathbb{I})$$, satisfying the axioms of a distributive lattice. (We don't want an inverse $$\neg: \mathbb{I} \to \mathbb{I}$$, since not all morphisms should be invertible.) It seems that with some modification, one can repeat most of the constructions of Riehl and Shulman in this simple setting. My suggestions:

• a morphism $$f: \text{hom}_A(a,b)$$ in a type $$A$$ from $$a:A$$ to $$b:A$$ is a map $$f: \mathbb{I} \to A$$ with identifications $$p_0: f(0) = a$$ and $$p_1: f(1) = b$$.
• the identity $$\text{id}_a: \text{hom}_A(a,a)$$ on $$a:A$$ is the constant map $$\text{const}_a: \mathbb{I} \to A$$ (with twice $$\text{refl}_a$$);
• for $$a:A$$, the 'under-category' type $$a/A$$ is the type of morphisms $$f: \mathbb{I} \to A$$ with $$p_0: f(0) = a$$.
• a map $$F: B \to A$$ is a covariant fibration if the induced map $$F_*: b/B \to F(b)/A$$ is an equivalence for any $$b:B$$, i.e. any morphism $$f: \text{hom}_A(F(b),a)$$ lifts to a 'unique' morphism $$\tilde{f}: \text{hom}_B(b,b')$$ starting in $$b:B$$ and projecting to $$f$$ under $$F$$. This implies that any morphism $$f: \text{hom}_A(a,b)$$ induces a map on fibers $$f_*: \text{fib}_F(a) \to \text{fib}_F(b),$$ so the fibers vary 'covariantly' in $$A$$.
• I call a type $$A$$ is covariant if the 'target map' $$t: a/A \to A$$ is a covariant fibration for all $$a:A$$. Since the fiber of $$t$$ over $$b:A$$ is $$\text{hom}_A(a,b)$$, every $$g: \text{hom}_A(b,c)$$ induces a 'post-composition' map $$g_*: \text{hom}_A(a,b) \to \text{hom}_A(a,c).$$
• One now checks that $$t: a/A \to A$$ is a fibration if and only if every square $$\require{AMScd} \begin{CD} b @>{g}>> c\\ @AfAA @AAA \\ a @= a \end{CD}$$ has a contractible type of 'solutions' $$H: \mathbb{I} \times \mathbb{I} \to A$$ with $$H(0,-) = f$$, $$H(-,0) = \text{id}_a$$ and $$H(-,1) = g$$. Restriction to the right vertical edge corresponds to $$g_*(f): \text{hom}_A(a,c)$$.
• It follows that for any covariant type, defining $$g \circ f :\equiv g_*(f): \text{hom}_A(a,c)$$ gives a composition of morphisms that is unital and associative: we have $$(\text{id}_b)_*(f) = f$$ and $$f_*(\text{id}_a) = f$$ by using the squares $$\lambda (s,t). f(t): \mathbb{I} \times \mathbb{I} \to A$$ and $$\lambda (s,t). f(s \land t): \mathbb{I} \times \mathbb{I} \to A$$: $$\require{AMScd} \begin{CD} b @= b\\ @AfAA @AAfA \\ a @= a \end{CD} \hspace{50pt} \begin{CD} a @>{f}>> b\\ @| @AAfA \\ a @= a, \end{CD}$$ and for associativity one proves (as in Corollary 5.6 of R+S) that the function type $$\mathbb{I} \to A$$ is again a covariant type for which we can apply the above square-filling (or 'cube-filling') criterion to the two morphisms (i.e. squares) $$\require{AMScd} \begin{CD} b @>{g}>> c\\ @AfAA @AA{g\circ f}A \\ a @= a \end{CD} \hspace{30pt} \text{ and } \hspace{30pt} \begin{CD} c @>{h}>> d\\ @AgAA @AA{h \circ g}A \\ b @= b, \end{CD}$$ and the resulting cube gives a proof of $$(h \circ g) \circ f = h \circ (g \circ f)$$.
• One can dualize everything above, defining contravariant fibrations $$F: B \to A$$ using 'over-category' types $$A/a$$ and call $$A$$ a contravariant type if $$s: A/a \to A$$ is a contravariant fibration for all $$a:A$$. One can now define a second composition by considering for $$f: \text{hom}_A(a,b)$$ the induced map $$f^*: \text{hom}_A(b,c) \to \text{hom}_A(a,c).$$ The composition $$g \circ_2 f :\equiv f^*(g)$$ is again unital and associative.
• I would like to define $$A$$ to be a category if $$A$$ is both a covariant and a contravariant type, i.e. the type family $$\text{hom}_A(a,b)$$ is both contravariant in $$a$$ and covariant in $$b$$. In this case the two compositions actually agree. To see this, one uses that there is a correspondence between squares of the form $$\require{AMScd} \begin{CD} b @>{g}>> c\\ @AfAA @AAA \\ a @= a \end{CD} \hspace{30pt} \text{ and } \hspace{30pt} \begin{CD} b @>{g}>> c\\ @AfAA @| \\ a @>>> c \end{CD}.$$ For example the map from right to left is given by sending the map $$H: \mathbb{I} \times \mathbb{I} \to A$$ to the map $$\lambda (s,t). H(s \wedge t,t)$$ that basically before applying $$H$$ first smashes the square onto the its upper left triangle with the right-bottom corner going to the left-bottom corner. These maps are fiberwise maps over the projection to $$(\mathbb{I} \to A) \times_A (\mathbb{I} \to A)$$ that only remembers $$f$$ and $$g$$, so if $$A$$ is both covariant and contravariant, they are automatically inverse equivalences (as then for each $$f$$ and $$g$$ there is an essentially unique such square). Furthermore both maps preserve the diagonal, and since going back and forth gives you another square that restricts to $$f$$ and $$g$$, this diagonal must be equal to either of the two composites.
• I haven't checked this in detail, but it seems to me that the Yoneda lemma $$C(a) \simeq \prod_{x:A} (\text{hom}_A(a,x) \to C(x))$$ should go through fine by just literally copying what Riehl and Shulman do.
• I think you are over estimating the complexcity of this (shape,tope) layer and so one. At the end of the day "all they do" is to add an object $I$ endowed with an order relation making $I$ an internal (i.e. it has top and bottom elements $0$ and $1$ and $x \leqslant y$ or $y \leqslant x$ for all $x,y$) exactly in the same way that you propose to add an object $I$. The reason why they single-out this type $I$ in a different layer of type theory is in order do define the notion of "extention type", which allows to actually define $hom_A(x,y)$ without using identity type. Aug 12, 2020 at 13:16
• Yeah I think to my unexperienced eye it seems like a lot of complexity for turning some propositional equalities into judgmental equalities. What would happen if one introduces $\text{hom}_A(x,y)$ as a formal type family, satisfying the rule that every $f: \mathbb{I} \to A$ gives a term $f': \text{hom}_A(f(0),f(1))$ and conversely every $f': \text{hom}_A(x,y)$ gives a map $f: \mathbb{I} \to A$ with judgmental equalities $f(0) \equiv a$ and $f(1)\equiv b$? Where does one run into problems? Aug 12, 2020 at 13:37
• So what you are describing is basically the definition of an extention type. Now, the thing is we don't want to be able to consider just the extention type corresponding to $hom_A(x,y)$, i.e. to the boundary inclusion $\Delta[0] \coprod \Delta[0] \to \Delta[1]$, but also these corresponding to more general simplicial maps. For e.g. the extention type along $\Lambda^1[2] \to \Delta[2]$ give you the type of arrows which are a composite of $f,g$ (a type which is contractible in a Segal type, but maybe not in general). Aug 12, 2020 at 13:59
• And there are an infinite number of maps you might want to consider extention type along. The role of the first two layer of their type theory is to determine which maps you are allowed to consider extention type along (basically, all inclusion between finite simplicial sets).... Of course I'm not saying that these extention type are neccessary, maybe what you are proposing can also works and extention type are just things that are there to make our lives easier. Aug 12, 2020 at 14:01

The shape/tope type theory is indeed just a "convenience". When I first suggested this approach to synthetic $$(\infty,1)$$-categories, I took the approach you describe with a simple axiomatic interval. But the coherence paths very quickly became much too complicated to deal with in practice; the shape/tope theory is just to make the endpoint equalities judgmental so that the coherence problems are manageable. We discussed this in the introduction of the paper:
For your second question, yes it makes sense to add some such axiom, but not about the universe of all types; you need to use a smaller "covariant" universe. The simplest one is a classifying type for covariant fibrations, which semantically represents the $$(\infty,1)$$-category of $$\infty$$-groupoids; you can also consider a classifying type for coCartesian fibrations, which would semantically represent the $$(\infty,1)$$-category of $$(\infty,1)$$-categories. The universe of all types is neither of these; even the internally defined "universe of Segal types" or "universe of discrete types" doesn't end up semantically with functions as morphisms, rather some kind of span. Various people are working on stating and modeling such axioms; the keyword to search for is directed univalence.