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

Question

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.

After reading the article, I had the following two questions:

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.

Answer 1

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:

In principle, all of the above theory could be developed within ordinary homotopy type theory, simply by axiomatically assuming the type 2 and its strict interval structure...These equalities are then data, which have to be carried around everywhere. This is quite tedious, and the technicalities become nearly insurmountable when we come to define commutative triangles, let alone commutative tetrahedra.

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.