Is univalence equivalent to every type function being a functor over equivalence?

Question

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]$$

Answer 1

Your axiom does not entail univalence.

It is consistent to add to type theory the isomorphism reflection rule $$\frac{\Gamma \vdash e : A \simeq B}{\Gamma \vdash A \equiv B}$$ which states that equivalent types are equal. A model validating this axiom is the cardinal model of type theory (see slide 24 of these slides). Isomorphism reflection entails UIP and is therefore inconsistent with Univalence.

We may interpret your axiom in the presence of isomorphism reflection by setting $f[e] \mathrel{{:}{=}} \mathrm{id}_{f(A)}$ where $f : \mathcal{U} \to \mathcal{U}$ is an endomap on a universe and $e : A \simeq B$. Indeed, from $e : A \simeq B$ and isomorphism reflection we get $A \equiv B$, therefore $f(A) \equiv f(B)$ and $f[e] = \mathrm{id}_{f(A)} : f(A) \simeq f(B)$.

Also, $f[e] = \mathrm{id}_A$ satisfies all the equations you proposed, except $\mathrm{id}_{\mathcal{U}}[e] = e$ – so I'd have to think about validating that one.