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

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

• Does the formulation of Univalence as saying that type equivalence is an Identity system already meet your criteria of not referring to type equality? Feb 20 at 20:58
• @MaxNew yes, that would as well. If this axiom is equivalent to univalence (assuming type equality exists), it will be equivalent to "type equivalence is an identity system" (without assuming type equality). Feb 20 at 21:03
• What is $f[e]$, a primitive type former? What is the corresponding elimination rule? Feb 20 at 21:10
• There's a related result in a paper by Steve Awodey at andrew.cmu.edu/user/awodey/preprints/uapl.pdf where he showed a weak form of univalence is equivalent to a "principle of invariance."
– aws
Feb 20 at 21:26
• Can you show the derivation? Feb 21 at 7:46

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.