# How do we use directed univalence in directed type theory?

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.

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.