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?



Univalence for weakly Tarski universes
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.


