15
$\begingroup$

The standard formulation of the univalence axiom for a universe type $U$ is that, for all $X : U$ and $Y : U$, the canonical map $(X =_U Y) \to (X \simeq Y)$ is an equivalence. As we (usually) cannot form the type of universe types, the usual univalence axiom is actually an axiom scheme, consisting of an instance of the univalence axiom for each universe type.

We can generalise (the form of) the univalence axiom as follows. Given a type $E (b)$ depending on $b : B$, we might say that $E (b)$ is univalent over $b : B$ if the canonical map $(b_0 =_B b_1) \to (E (b_0) \simeq E (b_1))$ is an equivalence. Of course, not all dependent types are univalent, but the univalence axiom for $U$ is precisely the condition that $X$ is univalent over $X : U$.

Question. Without mentioning universes (or otherwise internalising the condition of being a universe type), could we formulate an axiom scheme or inference rule that is equivalent to the usual univalence axiom scheme in the presence of universe types?

One consequence of the usual univalence axiom scheme is that, for every type $E (b)$ depending on $b : B$, there is a type $E' (b')$ univalent over $b' : B'$ and a map $\chi : B \to B'$ such that $E (b) \equiv E' (\chi (b))$. Indeed, given a univalent universe $U$ such that, (for every $b : B$) $E (b) : U$, we may take $B' \equiv U$, $E' (b') \equiv b'$, and $\chi \equiv (\lambda b : B . E (b))$. Anyway, we can take the image factorisation of $\chi$ to replace $B'$ with something smaller, but I'm not sure if this can be done respecting the judgemental equality $E (b) \equiv E' (\chi (b))$. If it could, it seems to me we would have a higher inductive type characterisation of $B'$ and $E'$. Applying this to a possibly non-univalent universe type would yield a univalent universe type, so by replacing "universe" with "univalent universe" in the appropriate places we would be able to interpret univalent type theory. Does this work?

$\endgroup$
11
  • 3
    $\begingroup$ Another way of talking about universes is that they are types of names, with a correspondence between names and the corresponding types, so this is an instance of a dependent type. For a dependent type to be a "universe" it must name "all" types, except that's not possible, so it names all types of a certain complexity. What actually matters is that the class of types that it does name should be closed under the other connectives, but these are not mentioned in stating univalence. (continued...) $\endgroup$ Commented Jan 13, 2022 at 13:52
  • 3
    $\begingroup$ (continued...) So yes, it is a good question to ask what univalence means for an arbitrary dependent type. It's a kind of "faithfulness": does every instance of equivalence between named types arise from an equality between their names? $\endgroup$ Commented Jan 13, 2022 at 13:53
  • 3
    $\begingroup$ Don’t have time to write a proper answer for now, but briefly: Yes, these are interesting ideas! Considering univalence for arbitrary type families not just universes (your 2nd para) has been there from the start — it was in Voevodsky’s original notes on univalence, and it’s phrased that way in Chris Kapulkin’s and my writeup of the simplicial model. The scheme you suggest in your 4th para is indeed a good one; phrased ∞-categorically, it is used in Nima Rasekh’s def of elementary ∞-topos. [cont’d] $\endgroup$ Commented Jan 13, 2022 at 14:50
  • 1
    $\begingroup$ The type theoretic version has certainly been informally discussed (re comparing elementary ∞-toposes with type theory), but I don’t know if anyone has written it up or developed it seriously. (NOTE: of course, I don’t want this answer-in-comments to block full answers — for whoever is inspired + has time to write a proper answer, please don’t feel inhibited to repeat what I’ve written here. If no-one else does then I may expand this later, but I don’t know when I’ll have good time.) $\endgroup$ Commented Jan 13, 2022 at 14:50
  • 3
    $\begingroup$ @მამუკა: In many formulations of dependent type theory (either syntax or models), the notion of “a type family dependent on some context” is a primitive notion, not involving assumption of any universe. $\endgroup$ Commented Jan 13, 2022 at 14:59

2 Answers 2

8
$\begingroup$

One possibility along these lines is large eliminations for higher inductive types. For instance, here is a large elimination rule for the higher inductive interval type $\mathsf{I}$ with $0,1:\mathsf{I}$ and $\mathsf{seg}:\mathsf{Id}_{\mathsf{I}}(0,1)$:

$$ \frac{\vdash A \,\mathsf{type} \quad \vdash B \,\mathsf{type} \quad \vdash e : \mathsf{Equiv}(A,B)}{x:\mathsf{I}\vdash E(x)\,\mathsf{type} \quad E(0)\equiv A \quad E(1) \equiv B \quad \mathsf{trans}^E_{\mathsf{seg}}= e} $$ (Everything in some ambient context $\Gamma$, of course.) Note that this can be stated without any universe, using only the "is a type" judgment that we always have in dependent type theory. (I'm assuming function extensionality here, so that it doesn't matter what kind of equality or homotopy we have in the final law $\mathsf{trans}^E_{\mathsf{seg}}= e$.)

Now suppose we have an interval type with this rule, and a universe type $\mathsf{U}$. Suppose moreover that the large elimination rule relativizes to $\mathsf{U}$, i.e. if $A$ and $B$ belong to $\mathsf{U}$ then so does $E$; this seems like a reasonable thing to include when "adding a universe type" to a theory that already had large eliminations. We will prove that $\mathsf{U}$ is univalent, using the encode-decode method.

Given $A,B:\mathsf{U}$, let $\mathsf{encode} : \mathsf{Id}_{\mathsf{U}}(A,B) \to \mathsf{Equiv}(A,B)$ be defined by transport or path induction; this is the map we want to show to be an equivalence. To define $\mathsf{decode}$ in the other direction, suppose given $e:\mathsf{Equiv}(A,B)$. Then by large elimination we have $E:\mathsf{I} \to \mathsf{U}$ with $E(0)\equiv A$ and $E(1)\equiv B$ and $\mathsf{trans}^E_{\mathsf{seg}}= e$. Now we can define $\mathsf{decode}(e) \equiv \mathsf{ap}_{E}(\mathsf{seg}) : \mathsf{Id}_{\mathsf{U}}(A,B)$. Then $\mathsf{encode}(\mathsf{decode}(e)) = \mathsf{trans}^E_{\mathsf{seg}}= e$. On the other hand, by path induction it's easy to prove $\mathsf{decode}(\mathsf{encode}(p)) = p$ for any $p:\mathsf{Id}_{\mathsf{U}}(A,B)$. Thus, $\mathsf{decode}$ is an equivalence, as desired.

To my knowledge, this was first observed in this post to the homotopy type theory mailing list in 2014, and I don't know of another reference. That discussion also considered "equivalence induction" (Corollary 5.8.5 in the HoTT Book) as a form of universe-free univalence, although as Peter noted in 2011 that can't be phrased without a universe type unless you add some other kind of polymorphism.

$\endgroup$
5
  • $\begingroup$ Of course, this is quite similar to the cubical approach that Dan discusses. But it predates it, and makes sense purely in Book HoTT. $\endgroup$ Commented Jan 14, 2022 at 6:50
  • $\begingroup$ Interesting. I find this unsatisfactory but I am unable to articulate why. I think I was hoping for an answer that would not only imply univalence in the presence of universes but also many of the universe-free consequences of univalence. For instance, iirc the univalence axiom gives us a way to construct the Rezk-completion of a 1-precategory. I guess large elimination for the higher inductive interval type alone is not enough. HIT groupoid quotients are enough. (Do we need large elimatiion here too?) Is this a general pattern? $\endgroup$
    – Zhen Lin
    Commented Jan 15, 2022 at 1:33
  • 1
    $\begingroup$ Yes, I think you need large elimination for the HIT groupoid quotient to construct Rezk completion, or at least to show that it is a Rezk completion. In general, pretty much anything you want to say about the identity types of a HIT requires large elimination. Thus the proposal for a universe-free version of univalence is really the general principle "large eliminations for all HITs" -- it just so happens that in the presence of a universe, large elimination for one particularly simple HIT is sufficient to imply full univalence. $\endgroup$ Commented Jan 15, 2022 at 17:16
  • 1
    $\begingroup$ Note also that semantically speaking, large eliminations for HITs are a version of descent for colimits in an $\infty$-category, which is one of the equivalent characterizations of $\infty$-toposes. $\endgroup$ Commented Jan 15, 2022 at 17:18
  • $\begingroup$ Most -- possibly all -- of the applications of univalence that I know fall in three groups: (1) those that follow from large eliminations for HITs, (2) those that inextricably involve a universe, like the construction of classifying spaces, and (3) function extensionality. $\endgroup$ Commented Jan 15, 2022 at 17:20
4
$\begingroup$

$\newcommand{\type}{\ \mathsf{type}}$ $\newcommand{\transp}{\mathsf{transport}}$ $\newcommand{\V}{\mathsf{V}}$ $\newcommand{\El}{\mathsf{El}\ }$

I'm uncertain if this satisfies your question, but most papers I've seen on cubical type theory introduce the machinery for univalence prior to the universe. They do this by having judgments that allow you to talk about things without universes that could only be talked about (in some sense) with universes in MLTT, and directly axiomatizing certain operations in terms of these judgments, rather than the universe.

For instance, the judgment:

$$Γ,i ⊢ A \type$$

is like a judgment that there is a path between types $A[i := 0]$ and $A[i := 1]$. And there is a rule like:

$$\frac{Γ,i ⊢ A \type \quad Γ ⊢ a : A[i := 0]}{Γ ⊢ \transp (i. A) \ a : A[i := 1]}$$

So, if you can judge that there is a path between types, you can transport values along it. Then there is a rule like:

$$\frac{Γ⊢E : A \simeq B}{Γ,i⊢ \V\ i\ E \type}$$

with $\V\ 0\ E = A$ and $\V\ 1\ E = B$. So, this already lets us judge that there is a path between equivalent types, and transport between them. There are additional details on how it all works, but it's all introduced before the universe, because it is used to define certain structure that the universe has.

I suppose one way of thinking of this is that it is directly axiomatizing univalence of the (too large to be a type) universe of all types. Then all universe types can be univalent just by declaring them to be proper sub-universes. That is, if you think of universe types as being inductive-recursive definitions:

$$\cal U \type \\u : \cal U ⊢ \mathsf{El}\ u \type$$

Then the image of $\mathsf{El}$ is in some sense already univalent. The content of the 'univalence axiom' is just to have a higher constructor of $\cal U$ that makes codes equivalent when they decode to equivalent types.$^1$ The decoding of this higher constructor is given by $\V$. You can actually do something like this in cubical Agda, where you can define a univalent inductive-recursive sub-universe of one of the in-built universes. You can also define a non-univalent I-R universe, but it is only non-univalent in the sense that $\El a \simeq \El b$ does not imply $a = b$ (i.e. the codes are too discrete). It does imply $\El a = \El b$ (path type, not judgmentally), and so on.

Perhaps one way to make this less reliant on special judgments, but still not reliant on universes, is to have an inherent identity type between types, similar to observational type theory. Then you can just state the univalence axiom for all types in a way that looks more obvious than cubical type theory. Then whether a universe is univalent comes down to whether code identity coincides with identity of decodings. Perhaps there is some subtle reason this wouldn't work out, though.

[1]: Someone can correct me if I'm mistaken, but something similar to this seems to come up when people talk about $\infty$-topoi. There is a universal presheaf on your $\infty$-topos that is univalent, but too big to live in the topos. Then the object classifiers (universe types) are all reflecting parts of that presheaf.

Generally you want "enough" object classifiers so that together they cover the entire too-large presheaf, which presumably means you can always work in terms of the classifiers. Postulating "enough" univalent universes directly is like postulating the object classifiers. I think the cubical approach is kind of like directly internalizing aspects of the universal presheaf without making it a proper type (which would be paradoxical). Then universes can be said to just reflect this structure that could already be talked about.

$\endgroup$
4
  • $\begingroup$ What does $\Gamma \vdash E: A \simeq B$ actually mean in the third rule? Is $\simeq$ a type constructor or is it an abbreviation for something? $\endgroup$ Commented Jan 13, 2022 at 22:06
  • 1
    $\begingroup$ It's an abbreviation for whichever variety of equivalence is preferred. You could also characterize it directly, I suppose. Most presentations just use the Voevodsky definition, I think. They only depend on some combination of Σ, Π and identity/path types over $A$ and $B$. $\endgroup$
    – Dan Doel
    Commented Jan 13, 2022 at 22:18
  • 1
    $\begingroup$ @FrançoisG.Dorais: It's a type, namely $(A \simeq B) := \Sigma (f : A \to B) . \Pi (y : B) . \mathsf{iscontr}(\mathsf{hfib}(f,y))$, where $\mathsf{hfib}(f,y) = \Sigma (x : A) \mathsf{Id}(f \, x, y)$ and $\mathsf{iscontr}(X) = \Sigma (x : X) . \Pi (y : X) . \mathsf{Id}(x, y)$. $\endgroup$ Commented Jan 14, 2022 at 10:49
  • $\begingroup$ Together with Mike's answer I think I now understand "why" univalence is said to be a theorem of cubical type theory! $\endgroup$
    – Zhen Lin
    Commented Jan 15, 2022 at 0:14

Your Answer

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