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.
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.