Introduce a rule in type theory that if $\Gamma \vdash f : \text{Type} \to \text{Type}$ and $\Gamma \vdash e : A \simeq B$ then $\Gamma \vdash f[e] : f(A) \simeq f(B)$.

It may seem like such a rule is redundant (of course type equivalence is preserved by operations on types), but that is not so. Assuming this axiom, $A \simeq B$ implies $A = B$ (because then $A = B$ is equivalent to $B = B$).

This is an interesting alternative to univalence because the axiom doesn't actually refer to type equality. (In a theory without type equality, it still implies that equivalent types satisfy all reflexive relations on types, and gives a way to transport arbitrary structures on equivalent types.)

My question is if this axiom is in fact *equivalent* to the univalence axiom.

I'm guessing that the following properties might also need to be assumed, but I'm not sure:

$$id_\text{Type}[e] = e$$ $$(f \circ g)[e] = f[g[e]]$$ $$f[id_A] = id_{f(A)}$$ $$f[e \circ d] = f[e] \circ f[d]$$