<p>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 &quot;the universe of <span class="math-container">$\infty$</span>-groupoids&quot;.  There is also a universe UCart sitting in between UCov and the whole U that is &quot;the universe of <span class="math-container">$(\infty,1)$</span>-categories&quot; (i.e. Segal types or maybe Rezk types), and this should also satisfy directed univalence.  You can read about it in <a href="https://arxiv.org/abs/2105.01724" rel="nofollow noreferrer">Synthetic fibered (∞,1)-category theory</a> by Buchholtz and Weinberger.  But the &quot;hom-types&quot; in the whole U are not functions but (at least in the semantics) some kind of correspondence.</p>
<p>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 &quot;amazing right adjoints&quot;.  The problem is that &quot;being a fibration&quot; is not a fiberwise condition, but involves transitions between objects of the base.</p>

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

<type-theory><dependent-type><homotopy-type-theory><homomorphism>
How do we use directed univalence in directed type theory?
Ilk
# How do we use directed univalence in directed type theory?

(Asked by: username_0 on 2022-03-09)

In [directed type theory of Riehl and Shulman](https://arxiv.org/pdf/1705.07442.pdf), 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](https://dl.acm.org/doi/abs/10.1145/3373718.3394794), 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.

**Tags:** type-theory, dependent-type, homotopy-type-theory, homomorphism

---

## 1 answers

### Answer by username_1 on 2022-03-09. Score: 4 | Accepted answer

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](https://arxiv.org/abs/2105.01724) 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.


---

