8
$\begingroup$

People would say in univalent type theory, anything you defined for types should respect equivalence since univalence told you equivalence equivalent to equality. But that's not correct. Only equivalence of types inside the same universe are to be respected. Because equality doesn't make sense for types in different universes, at least in any direct way.

However, it seems if only your definition is universal polymorphic, it should still preserve equivalence. It's my vague intuition, so maybe I am wrong. Whatever, there is no univalence in this case so you cannot just do transport to prove the invariance. So is my claim correct? And is there any general version of univalence that could help?

$\endgroup$
5
  • $\begingroup$ You may lift the lower-leveled type to a higher level and use univalence, and lifting is an embedding, so you can undo it after some transports. $\endgroup$
    – ice1000
    Commented Feb 22, 2022 at 20:40
  • $\begingroup$ Yep. Then you know that your construction P induces equivalence between lift X and lift Y. But how do you know that P X is equivalent to P (lift X)? Basically it's the same problem. $\endgroup$ Commented Feb 23, 2022 at 16:17
  • $\begingroup$ Even more serious, if you have a commutative diagram of equivalences, involving types in different universes, the equivalences induced by P should also give commutative diagram of the same shape. This coherence problem can be solved by path algebra if one has univalence. $\endgroup$ Commented Feb 23, 2022 at 16:20
  • $\begingroup$ Would it help to have cumulative universes, so that lift is the identity? $\endgroup$ Commented Feb 26, 2022 at 0:44
  • $\begingroup$ I don't know much about universal polymorphism with cumulativity. But it sounds like a way to answer. $\endgroup$ Commented Feb 27, 2022 at 17:21

1 Answer 1

4
$\begingroup$

At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths:

$$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$

The top being a 'type path' and the bottom being a 'term path'. Because these are judgments, you can't work with them as hypotheses exactly. But there are derived constructions like:

$$\frac{Γ,i⊢T\ \mathsf{type}\qquad Γ⊢ t_0 : T[i := 0]}{Γ ⊢ \mathsf{transport}_i\ T\ t_0 : T[i := 1]}$$

So, if you can judge that a path exists in types, then you can transport by it. Further, the $\mathsf{Glue}$ type (or whatever equivalent is used) lets you judge that a path exists based only on an equivalence. Something like (using $\mathsf{V}$ because it's simpler than $\mathsf{Glue}$):

$$\frac{Γ ⊢ e : Σ_{f : A → B}\ \mathsf{isEquiv}\ f}{Γ,i ⊢ \mathsf{V}_i\ e\ \ \mathsf{type}}$$

If you have a type path judgment, you can also abstract paths over it, I believe. So:

$$\frac{Γ,i ⊢ P\ \mathsf{type}\quad Γ ⊢ x : P[i := 0]\quad Γ ⊢ y : P[i := 1]}{Γ ⊢ \mathsf{Path}_{i. P}\ x\ y\ \mathsf{type}}$$

Note that none of this requires knowing that $A$ and $B$ belong to a common universe. If we can judge that $A$ and $B$ are types, we can judge that the type of $e$ is a valid type, build values, judge that $\mathsf{V}$ is a valid type (path), and transport through it. Judgmental rules say that $\mathsf{V}_0\ e = A$ and $\mathsf{V}_1\ e = B$. And we can talk about the type of values related by that path. In some sense, this is building univalence, "for all types," not just for a universe, although perhaps you could imagine that "all types" form a very large, implicit universe of sorts.

Now, strictly speaking, Agda doesn't work this way. It doesn't really have this 'judgment of types' prior to the classification of types by a universe. Rather, it is designed around the idea that every type has an intrinsic universe, and there are enough universes that you can get away with never talking about the $\mathsf{type}$ judgment directly, as a user. However, this means that all of the above stuff gets parameterized by a universe in Agda, and you are back to the univalent universe scenario, because $\mathsf{type}$ gets replaced with $: \mathsf{Type}_n$, and there's no way for $n$ to vary with $i$ (universes of different levels are not equivalent). I'm also not familiar with any comparable proof assistant (like, based in something resembling MLTT) that doesn't work this way, although I'm far from having tried everything.

So this can be seen as a point in favor of not structuring around a fixed hierarchy of universes, and instead letting universes be incidental reflections of parts of the totality of types. There are still some things that can't be spoken about without identifying a universe to work in (unless you add other features that aren't even present in most paper presentations of type theory). But it at least changes, "equivalence between types is respected if they belong to a common univalent universe," into something more like, "a universe is univalent if equality of its codes reflects the path judgment of the decodings."

On the flip side, you actually can try out this strategy in Agda by ignoring its universe hierarchy and polymorphism, and just working in $\mathsf{Type}_0$. Because that universe is closed under (higher) induction-recursion, you can introduce (univalent) universes internal to it, and the cubical machinery on $\mathsf{Type}_0$ works like the judgmental presentation in papers. Essentially $\mathsf{Type}_0$ is a model of (something like) the paper theory. I'm not familiar with what sort of tooling people imagine using with this sort of 'a la carte' universe classification, though, so it might get tedious for complicated situations due to a lack of such features in Agda.

So, on the one hand, you could say that Agda's (and others') design is lacking in certain ways. On the other hand, it has a feature (that seems often viewed with suspicion, and goes unused) that makes a small subtheory of it into a model of the 'improved' design that people would typically use, and you could try it out today.

I guess I'm uncertain if this answers your exact questions. Agda's universe polymorphism is an example of something that's actually very tedious to model using induction-recursion. I think the hope is that you could instead think less about universe 'arithmetic' in favor of always conjuring up the exact 'universe that pertains to this problem.' And then $\mathsf{Type}_0$ or the $\mathsf{type}$ judgment is the universe of everything anyone could possibly want to talk about, and everything defined on it is invariant under equivalence. So in that sense, it hopefully answers your question in the affirmative.


Addendum: here's an example of the sort of thing you can do. Suppose we have a type $L$ of levels, and a bunch of universes:

$$\mathsf{U} : L → \mathsf{Type}_0 \\ \mathsf{El} : \prod_{\ell:L} \mathsf{U}_\ell → \mathsf{Type}_0$$

Then we can define their union as a HIT:

module _
  (L : Type)
  (U : L → Type)
  (El : ∀{ℓ} → U ℓ → Type)
  where
  variable
    ℓ : L
    s t : U ℓ

  data ⋃U : Type where
    ι : U ℓ → ⋃U
    un : El s ≃ El t → ι s ≡ ι t

  ⋃El : ⋃U → Type
  ⋃El (ι x) = El x
  ⋃El (un e i) = ua e i

It doesn't really matter whether $\mathsf{U}_\ell$ was univalent, because we are imposing univalence on $\bigcup\!\mathsf{U}$. But at the same time, we are ensuring that families with type $\bigcup\!\mathsf{U} → \mathsf{Type}_0$ are defined in a more 'parametric' way. You can't just look at the $L$ values and do something different based on them, because you have to give equivalent answers for equivalent types regardless of which $\mathsf{U}_\ell$ they came from. Presumably it's not as parametric as not being able to inspect the values at all, but I'm not sure it's possible to do much better without more language features.

Anyhow, if we imagine that $F : \bigcup\!\mathsf{U} → \mathsf{Type}_0$ is a 'universe polymorphic' family, we can write the following:

  inst : (⋃U → Type) → U ℓ → Type
  inst F = F ∘ ι

  lemma : (F : ⋃U → Type) → El s ≃ El t → inst F s ≡ inst F t
  lemma F e = cong F (un e)

i.e. $\mathsf{inst}$ instantiates the polymorphic family to one of the universes, and if we apply the family to equivalent types, even in distinct universes, we can transport between the results.

If you want to decouple the level from the type, instead of packing them together like this example, and say that a definition in Agda with type like $(\ell : \mathsf{Level}) → \mathsf{Type}_\ell → ...$ satisfies an analogous property, then presumably you need something more like parametricity about $\mathsf{Level}$. This is because levels of distinct universes can't just be equal/have a path between them (or the universes would be equivalent), so there needs to be some looser sort of 'connection' between universe levels that, when combined with a Π type over $\mathsf{Level}$, yields the desired 'univalence across levels' principle.

$\endgroup$
2
  • $\begingroup$ Yeah, that's very closed to what I thought. I feel people could invent some type theory with essentially different rules for different univalent universes, and that will make my claim ridiculous. But definitely not for recent "paper" type theory or for cubical agda. $\endgroup$ Commented Feb 24, 2022 at 9:51
  • $\begingroup$ However, I still wonder how such a meta-theorem could be stated in a rigor way. For example, a procedure that could automatically generate a proof that universal polymorphisms, or at least constructions "uniform for all universes", are invariant under equivalences? $\endgroup$ Commented Feb 24, 2022 at 9:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.