I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web.
For some time I was a bit upset about this. But maybe this is our fault, by often trying to explain univalence only imprecisely, mixing the explanation of the models with the explanation of the underlying theory (MLTT, identity types, universe), with none of the two explained sufficiently precisely.
There are long, precise explanations such as the HoTT book, for example, or, the formalizations in Coq, Agda and Lean.
But perhaps we don't have publicly available material with a self-contained, brief and complete formulation of univalence, so that interested mathematicians and logicians can try to contemplate the axiom in a fully defined form.
Here is an attempt to rectify this:
This also has an ancillary Agda file with univalence defined from scratch (without the use of any library at all). Perhaps somebody should add a Coq "version from scratch" of this.
M.