How to formulate the univalence axiom without universes?

Question

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?

Answer 1

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.

Answer 2

$\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.