Thinking about the recently re-mentioned characterization of univalence in terms of a map Equiv A B -> (A = B) that is only assumed to be a section of the canonical map in the other direction, it occurred to me that this gives a way to state the univalence axiom without first needing any "coherent" notion of equivalence. For at least if we have funext to start with, then equalities in Equiv A B are (for any coherent definition of Equiv A B) equivalent to equalities in A -> B, so we can state the retraction property in terms of those. More precisely, let coe : (A = B) -> A -> B be coercion along an equality, and let QInv A B := Sigma(f:A->B) Sigma(g:B->A) ( (Pi(x:A) g(f(x)) = x) \times (Pi(y:B) f(g(y))=y) ) be the type of quasi-invertible functions (incoherent equivalences). We know that it is inconsistent to ask that the map (A = B) -> QInv A B induced by coe is quasi-invertible. But suppose we instead ask for just ua : QInv A B -> (A = B) and uabeta : Pi((f,g,a,b) : QInv A B) Pi(a:A), coe (ua (f,g,a,b)) a = f(a) If full univalence holds, then such functions certainly exist, since any quasi-inverse can be improved to a coherent equivalence. But conversely, if we assume funext to start with, then the full univalence axiom can be proven from this ua and uabeta. (I just formalized this in Coq to be sure.) Maybe other people have already observed this, but I don't think I noticed it before. It means that we don't need to invent or motivate a coherent notion of equivalence before stating (or, in cubical type theory or a semantic model, proving) univalence. Instead we can state univalence in this way, and then (having already motivated funext, which is much easier, and also has a "weak improves to strong" theorem) motivate the search for a "good" definition of Equiv A B as "can we define more explicitly a type that is equivalent to A = B"? Mike