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?
Best Answer
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.