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 $f(0) = a$ and $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 $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.