6
$\begingroup$

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?

$\endgroup$

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.