7
$\begingroup$

I've started reading Riehl and Shulman's A type theory for synthetic $\infty$-categories, which looks like it develops some beautiful theory, but I want to make sure I'm not misunderstanding some of the initial formalities. In particular, I want to make sure I understand the constructor for function types out of shapes.

For instance, recall $\Delta^1:\equiv\{t:\mathbb{2}\space\vert\space\top\}$ (for definitions and formal deduction rules I refer you to the linked paper). Now, as I understand it, given a type $A$, to define a non-dependent function $\Delta^1\rightarrow A$ (shorthand for $\langle \Delta^1\rightarrow A\space\vert\space^{\bot}_{\text{rec}_\bot}\rangle$), we need a term $a$ (possibly containing $t$ free) such that $\{t:\mathbb{2}\space\vert\space\top\}\vdash a:A$; then $(\lambda t.a):\Delta^1\rightarrow A$. The problem is, I don't see how to define any non-constant functions of this kind (ie functions where $a$ has non-trivial dependence on $t$).

I believe the only non-trivial rule for constructing type elements that depend on shape variables is the given recursion principle for disjunction of topes, which says that if $\{t:I\space\vert\space\varphi\}\vdash a_\varphi:A$, $\{t:I\space\vert\space\psi\}\vdash a_\psi:A$, and $\{t:I\space\vert\space\varphi\wedge\psi\}\vdash a_\varphi\equiv a_\psi$, then $\{t:I\space\vert\space\varphi\vee\psi\}\vdash \text{rec}^{\varphi, \psi}_\vee(a_\varphi, a_\psi):A$, with computation rules given by $\{t:I\space\vert\space\varphi\}\vdash \text{rec}^{\varphi, \psi}_\vee(a_\varphi, a_\psi)\equiv a_\varphi$ and $\{t:I\space\vert\space\psi\}\vdash \text{rec}^{\varphi, \psi}_\vee(a_\varphi, a_\psi)\equiv a_\psi$. So, for instance, defining non-trivial functions out of the boundary $\partial\Delta^1:\equiv \{t:\mathbb{2}\space\vert\space t\equiv 0\vee t\equiv 1\}$ is easy: just choose terms $a_0, a_1:A$, and then $\lambda t.\text{rec}^{t\equiv 0, t\equiv 1}_\vee(a_0, a_1):\partial\Delta^1\rightarrow A$.

However, I cannot see any way of writing $\top$ as a disjunction that would allow this recursion principle to be useful for maps out of $\Delta^1$. In particular, I do not understand how we would inhabit a $\text{hom}$ type with non-trivial elements; recall that given a type $A$ and terms $x, y:A$, we define $\text{hom}_A(x, y):\equiv\langle\Delta^1\rightarrow A\space\vert\space^{\partial\Delta^1}_{\text{rec}^{t\equiv 0, t\equiv 1}_\vee(x, y)}\rangle$. It seems to me that the only way we can inhabit this type (with only the rules given so far) is if $x\equiv y$, and in this case the only inhabitant we can construct is $\lambda t.x$. (Which is imagine is supposed to correspond to the "identity morphism" at $x$?)

As a first question, I would just like someone to confirm for me that this is a correct understanding. As a second question, if that is the case, this situation seems to me comparable to the fact that the only constructor for identity types in undirected HoTT is $\text{refl}$. Indeed, if I remember correctly, it is relatively consistent in Martin-Lof type theory without univalence for every type to be a set. However, once one has univalence, then one can begin constructing non-trivial paths – for instance, the path induced by the non-trivial auto-equivalence of $\mathbf{2}$. So, my question is whether there is anything analogous in Riehl and Shulman's theory. A priori can one exhibit a type with a non-trivial $\text{hom}$ type? And if not, is there a "directed analog" of the univalence axiom that would allow us to construct them?

Bear in mind that I haven't yet read the paper in any detail, so apologies if this is discussed somewhere within it – I want to make sure that I'm understanding these preliminaries before tackling the paper in full. Also, if possible, I would prefer answers that don't depend too heavily on the semantic interpretation of this theory in Segal spaces, as I am not well-versed in the latter. I do know basic definitions though so could (hopefully) follow if that language is necessary to answer the question properly.

$\endgroup$

1 Answer 1

1
$\begingroup$

You're correct that in our type theory without additional axioms, there are no nontrivial closed terms in hom-types. (Of course, by hypothesizing elements of hom-types, we can produce other elements of hom-types.) Thus, the theory is only potentially a theory of $(\infty,1)$-categories, in the same way (as you said) that MLTT is potentially a theory of $\infty$-groupoids. Directed univalence is a subject of current research; Cavallo-Riehl-Sattler have proven a form of it in the bisimplicial model, and Weaver-Licata have a constructive version in a bicubical model, but I don't think any of it has appeared publically yet.

$\endgroup$
1
  • 1
    $\begingroup$ I think that's probably just a typo and we should have written $\equiv$. $\endgroup$ Apr 4, 2020 at 14:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .