How do we use directed univalence in directed type theory?

Question

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.

Answer 1

If by UKan you mean the ambient universe of all types in the theory (which is a bit of a misnomer, since there is no real Kan-ness to them), then no, it is not Segal. You should think of UCov as "the universe of $\infty$-groupoids". There is also a universe UCart sitting in between UCov and the whole U that is "the universe of $(\infty,1)$-categories" (i.e. Segal types or maybe Rezk types), and this should also satisfy directed univalence. You can read about it in Synthetic fibered (∞,1)-category theory by Buchholtz and Weinberger. But the "hom-types" in the whole U are not functions but (at least in the semantics) some kind of correspondence.

And no, unfortunately there does not seem to be any way to define universes like UCov and UCart internally in the model, at least not without stipulating further additional structure such as "amazing right adjoints". The problem is that "being a fibration" is not a fiberwise condition, but involves transitions between objects of the base.