univalence without coherent equivalences

[Michael Shulman <shu...@sandiego.edu>]

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