In Martin-Löf type theory, a weakly Tarski universe is a type $\mathcal{U}$ with a type family $\mathcal{T}(A)$ indexed by terms $A:\mathcal{U}$, which is closed under identity types, dependent products, and dependent sums: there are functions
$$\Sigma_\mathcal{U}:\prod_{A:\mathcal{U}} (\mathcal{T}(A) \to \mathcal{U}) \to \mathcal{U}$$
$$\Pi_\mathcal{U}:\prod_{A:\mathcal{U}} (\mathcal{T}(A) \to \mathcal{U}) \to \mathcal{U}$$
$$\mathrm{Id}_\mathcal{U}:\prod_{A:\mathcal{U}} \mathcal{T}(A) \to (\mathcal{T}(A) \to \mathcal{U})$$
with equivalences
$$\mathrm{equiv}_{\Sigma}(A, B):\mathcal{T}(\Sigma_\mathcal{U}(A, B)) \simeq \sum_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$
$$\mathrm{equiv}_{\Pi}(A, B):\mathcal{T}(\Pi_\mathcal{U}(A, B)) \simeq \prod_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$
$$\mathrm{equiv}_{\mathrm{Id}}(A, a, b):\mathcal{T}(\mathrm{Id}_\mathcal{U}(A, a, b)) \simeq a =_{\mathcal{T}(A)} b$$
A weakly Tarski universe is a strict Tarski universes if the equivalences are promoted to definitional equalities:
$$\mathcal{T}(\Sigma_\mathcal{U}(A, B)) \equiv \sum_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$
$$\mathcal{T}(\Pi_\mathcal{U}(A, B)) \equiv \prod_{x:\mathcal{T}(A)} \mathcal{T}(B(x))$$
$$\mathcal{T}(\mathrm{Id}_\mathcal{U}(A, a, b)) \equiv a =_{\mathcal{T}(A)} b$$
In both cases, we can define the internal equivalence types $A \simeq_\mathcal{U} B:\mathcal{U}$ for $A:\mathcal{U}$ and $B:\mathcal{U}$.
There are two definitions of univalent Tarski universes possible: that the canonical transport function
$$\mathrm{transport}^\mathcal{T}(A, B):A =_\mathcal{U} B \to \mathcal{T}(A) \simeq \mathcal{T}(B)$$
is an equivalence of types, and that the canonical function
$$\mathrm{idtoequiv}(A, B):A =_\mathcal{U} B \to \mathcal{T}(A \simeq_\mathcal{U} B)$$
is an equivalence of types. In strict Tarski universes, these two definitions of univalent universes are the same, because the two types $\mathcal{T}(A \simeq_\mathcal{U} B)$ and $\mathcal{T}(A) \simeq \mathcal{T}(B)$ are definitionally equal to each other
$$\mathcal{T}(A \simeq_\mathcal{U} B) \equiv \mathcal{T}(A) \simeq \mathcal{T}(B)$$
However, in weakly Tarski universes, the two types are only equivalent to each other by the function
$$\mathrm{equiv}_{\simeq}:\mathcal{T}(A \simeq_\mathcal{U} B) \simeq (\mathcal{T}(A) \simeq \mathcal{T}(B))$$
derived from $\mathrm{equiv}_{\Sigma}$, $\mathrm{equiv}_{\Pi}$, and $\mathrm{equiv}_{\mathrm{Id}}$.
Is it still true that every weakly Tarski universe which is univalent by $\mathrm{transport}^\mathcal{T}$ is also univalent by $\mathrm{idtoequiv}$, and is it still true that every weakly Tarski universe which is univalent by $\mathrm{idtoequiv}$ is also univalent by $\mathrm{transport}^\mathcal{T}$? If not, under what conditions do the two notions of univalence for weakly Tarski universes coincide?
Best Answer
Yes, $\mathrm{transport}^\mathcal{T}$ is an equivalence if and only if $\mathrm{idtoequiv}$ is an equivalence. To show this, it is enough to prove that the underlying functions of $\mathrm{transport}^\mathcal{T}(p)$ and $\mathrm{equiv}_\simeq (\mathrm{idtoequiv}(p))$ are equal for all $p : A =_\mathcal{U} B$. By path induction, it is enough to show that $\mathrm{equiv}_\simeq$ maps the identity function in $\mathcal{T}(A \to_\mathcal{U} A)$ to the identity function in $\mathcal{T}(A) \to \mathcal{T}(A)$, but the identity function in $\mathcal{T}(A \to_\mathcal{U} A)$ is defined as $\mathrm{equiv}_\simeq^{-1}(\lambda x.x)$, so this is true.