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?

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 typesof 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$6more comments