I’ll give first a simplicial definition of univalence, and then a type-theoretic one, and discuss the equivalence between them as we go.
The first thing to know is that univalence is a property that can be defined for any family of types, or in models, for any fibration. The Univalence Axiom then says that a particular family of types — a “universe” — is univalent. I’ll come back to the universe at the end.
So: what is univalence for a fibration? Roughly, a fibration is univalent just when the map from “paths in the base” to “equivalences between fibers” is itself an equivalence.
Precisely: given two fibrations $Y_1, Y_2$ over a common base $X$, write $\newcommand{\Hom}{\mathcal{Hom}}\Hom_X(Y_1,Y_2)$ for the fibred mapping space between them, i.e. the exponential in $\newcommand{\SSet}{\mathbf{SSet}}\SSet/X$, which represents maps between (pullbacks of) $Y_1$ and $Y_2$, and write $\newcommand{\Eqv}{\mathcal{Eqv}}\Eqv_X(Y_1,Y_2)$ for the subobject of $\Hom_X(Y_1,Y_2)$ that represents equivalences between them. So an $n$-simplex of $\Eqv(Y_1,Y_2)$ over a simplex $x \in X_n$ corresponds to an equivalence of fibers $(Y_1)_x \to (Y_2)_x$ over $\Delta[n]$.
Now, given a single fibration $Y$ over $X$, we can consider maps between different fibers of $Y$ by first pulling it back to $X \times X$ along the two projections $\pi_1$, $\pi_2$. So $\pi_1^*(Y)_{(x_1,x_2)} \cong Y_{x_1}$, and $\pi_2^*(Y)_{(x_1,x_2)} \cong Y_{x_2}$. Now consider the fibred space of equivalences between these: $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$. So an element of this over $(x_1,x_2)$ represents an equivalence $Y_{x_1} \to Y_{x_2}$ between fibers of $Y$.
There’s always a map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$, living over the diagonal $\Delta_X : X \to X \times X$, where $i(x)$ represents the identity map $Y_x \to Y_x$. Then we define: the fibration $Y \to X$ is univalent if this map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ is a weak equivalence.
Some easily equivalent forms:
- (in $\SSet$, or anywhere else where cof = mono) $i$ is a trivial cofibration;
- $i$ makes $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ a path object for $X$;
- the induced map $P(X) \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ over $X \times X$ is an equivalence (for any other path object $P(X)$).
A slightly-less-trivially equivalent form is the same statement, but using an alternative construction of the object of equivalences — call it $\Eqv'_X(Y_1,Y_2)$ — which represents not just “equivalences from $Y_1$ to $Y_2$”, but “maps $f$ from $Y_1$ to $Y_2$, equipped with a homotopy left inverse $(g_l, \alpha)$ (where $\alpha$ is the homotopy $g_l \cdot f \to 1_{Y_1}$) and a homotopy right inverse $(g_r,\beta)$”. This is equivalent to the other versions just since the evident projection $\Eqv'(Y_1,Y_2) \to \Eqv(Y_1,Y_2)$ is always a trivial fibration.
Now let’s move to type theory. First a couple of notes about language. It’s familiar in homotopy theory to think of a fibration as a family of spaces varying over a base space. In type theory, this is literally the case in the language — you work with a family of types indexed by a variable varying over a base type, just like in traditional settings you work with the family of sets $\newcommand{\R}{\mathbb{R}}\newcommand{\N}{\mathbb{N}}\R^n$ indexed by $n \in \N$ — but such a family will generally behave like a fibration, not just like a discretely indexed family of discrete sets. And in the simplicial model (and other similar models), a family of types gets interpreted as a fibration.
Also, like the HoTT book, I’ll work in prose, not in formal symbolic type theory, just like how when one does maths over a traditional foundation, one writes in prose rather than the formal symbols of first-order set theory. (In fact the gap between prose and formal language is significantly smaller in type theory than in set-theoretic foundations, for most mathematics.)
The only basic notions we need are path types, function types, and $\Sigma$-types (types of tuples of data).
Given two types $Y_1$, $Y_2$, we can define the type $\newcommand{\tyEqv}{\mathsf{Eqv}}\tyEqv(Y_1,Y_2)$ of equivalences between them as the type of tuples $(f,g_l,\alpha,g_r,\beta)$, where $f$ is a function $Y_1 \to Y_2$, $g_l$ is a function back the other way, $\alpha$ is a function giving for each $y \in Y_1$ a path from $g_l(f(y))$ to $y$ (so $(g_l,\alpha)$ together are a homotopy left inverse for $f$), and similarly $(g_r,\beta)$ is a homotopy right inverse. Saying a function $f : Y_1 \to Y_2$ is an equivalence means equipping it with suitable $(g_l,\alpha,g_r,\beta)$.
In general, $Y_1$ and $Y_2$ may have been dependent all along on some variable(s) — say, $Y_1(x)$ and $Y_2(x)$, where $x$ ranges over some other type $X$. Then their interpretations in the simplicial model will be fibrations $[Y_i] \to [X]$; and $\tyEqv(Y_1(x),Y_2(x))$ is itself dependent on $x : X$, so its interpretation is also a fibration $[\tyEqv(Y_1,Y_2)] \to [X]$. And in fact this comes out to be precisely $\Eqv'([Y_1],[Y_2])$ as defined above, since path-types are modelled by (fibred) path-objects and function types by (fibred) mapping objects.
Now for a type $Y(x)$ depending on $x:X$, and for any $x_1,x_2 : X$, there’s a canonical map $\newcommand{\tyP}{\mathsf{P}}i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$, defined by giving the identity equivalence $Y(x) \to Y(x)$ on reflexivity paths. (To construct something depending on a general path, it’s enough to construct it for reflexivity paths; this is the defining property of path-types, and is analogous to extending maps defined on $X$ to maps defined on a path-object $P(X)$ along the inclusion $X \to P(X)$.)
Now, say that a family of types $Y(x)$, indexed by $x : X$, is univalent if this map $i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$ is an equivalence for each $x_1,x_2 : X$.
I hope the remarks so far about interpretation make it reasonably plausible, if not quite watertight, why a family of types is univalent in this sense just if its interpretation as a fibration is univalent in the simplicial sense.
Now, in type theory (as in other foundations), one often wants to consider a universe — a family of types closed under common constructions (e.g. forming function types). Indeed, one may consider multiple such universes. The Univalence Axiom, for a given universe, says just that this universe, considered just as a family of types, is univalent.
I’ll stop here, because this is plenty long enough already! But a full treatment of all the above, together with the construction of univalent universes in $\SSet$, can be found in The Simplicial Model of Univalent Foundations (Kapulkin, Lumsdaine, Voevodsky). Specifically, it’s in Section 3, using the universe introduced in in Section 2; you can probably comfortably skip Section 1, which is about the technicalities of constructing models of type theory, and also most of Section 2 after the universe is constructed.
Consider the relativized constructibility hypothesis, which asserts that $V=L[A]$ for some set $A$.
This axiom is compatible with any locally verifiable large cardinal property, properties that can be witnessed by a certain fact inside some sufficiently large $V_\theta$. See my blog post, local properties in set theory for more discussion of this, including the fact that the locally verifiable properties are precisely the $\Sigma_2$ properties.
Many large cardinal properties are locally verifiable, including: weak compactness, Ramsey, subtle, measurable, measurable with specified $o(\kappa)$, superstrong, almost huge, huge, I0, I1, I2, and others. These notions span a huge part of the large cardinal hierarchy. All these notions are relatively consistent with the hypothesis $\exists A\ V=L[A]$.
Meanwhile, many other large cardinal properties are not locally verifiable, since they require one to have witnesses for arbitrarily large ordinals, making the properties $\Pi_3$ rather than $\Sigma_2$. For example, reflecting cardinal, strong, strongly compact, supercompact, extendible, superhuge and others. None of these notions is consistent with $\exists A\ V=L[A]$.
Best Answer
Still not an answer to the second question, but I wanted to add something else that's missing: in fact the bare statement $(A=B)\simeq (A\simeq B)$ is not known to be a correct form of the univalence axiom. The correct statement is that the canonical map $(A=B) \to (A\simeq B)$ is an equivalence. The statement $(A=B)\simeq (A\simeq B)$ can be regarded as an abusive abbreviation of this, in the same way that mathematicians often write "$A\cong B$" to mean that some canonical map $A\to B$ is an isomorphism, but to be precise we have to be careful.
There is now a much weaker-looking known equivalent form of the univalence axiom, see here. However, it does still use pointwise homotopies in the equivalences that are to be made into equalities. I suspect that the corrected form "the canonical map $(A=B) \to (A\cong B)$" of your second question is indeed strictly weaker than univalence in the absence of funext, but I don't know.