In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions. I will call the main universe $UKan$ to distinguish from $UCov$.
We have a Yoneda lemma, saying that given Segal type $A$ for any covariant $C : A \rightarrow UKan$ and $a : A$ we have a pair of inverse equivalences between $C(a)$ and $\Pi_{x:A} hom_A\:a\:x \rightarrow C(x) $, where being Segal is a particular condition on $A$.
Now the standard form of Yoneda lemma as used informally in functional programming tends to have $A = U$ and treats the resulting $hom_{U}\:a\:x$ as a function $a \rightarrow x$, when applied at $C$ being a covariant endofunctor. In the formal setting of directed type theory this $U$ should be $UKan$.
This seems to be akin to directed univalence, but directed univalence only works for a smaller universe $UCov$, which would also discharge the assumption that A has to be Segal as $UCov$ is itself Segal. Is $UKan$ itself Segal and can we strengthen the $hom$ to a function as we are working with a covariant family with domain in only $UKan$ instead of the stronger $UCov$ in this particular application?
This brings me to another question is there a way to carve out $UCov$ in the directed type theory without appealing to models? I had one idea that would be to define $UCov$ as $\Sigma_{A:UKan}isCov(\lambda(x:\top).A)$, but this is always covariant and as such does not have the desired effect. Is there a nice internal way to define $UCov$ without appealing to closure properties in the model, i.e. carving it out as $\Sigma_{A:UKan}CovDef\:A$, for some internal $CovDef : UKan \rightarrow UKan$?
Any references to paper sections I might have missed are welcome.