5
$\begingroup$

Let us consider Martin-Löf type theory with a cumulative hierarchy of universes $$ \mathcal{U}_0\colon\mathcal{U}_1\colon\ldots $$ If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\mathcal{U}_i} B:\mathcal{U}_i$. Using the axiom of cumulative hierarchy, we can derive $A, B:\mathcal{U}_{i+1}$, so we have also an identity type $A=_{\mathcal{U}_{i+1}}B$. Assuming the Univalence axiom (for all the universes), they are both equivalent to a type of equivalences $(A\simeq B)$, which has nothing to do with universe issues. What can we say about the relationship between types $A=_{\mathcal{U}_i} B$ and $A=_{\mathcal{U}_{i+1}} B$ without the Univalence axiom?

$\endgroup$
3
$\begingroup$

In general cummulative universes are a bit nasty. To see what is really going on, at the very least it makes sense to have explicit lifting maps $\mathsf{lift}_{i,j} : \mathcal{U}_i \to \mathcal{U}_j$ for $i \leq j$. With these in place, your question is: how do the types $$\mathsf{lift}_{i,i+1}(A =_{\mathcal{U}_i} B)$$ and $$(\mathsf{lift}_{i,i+1} A) =_{\mathcal{U}_{i+1}}(\mathsf{lift}_{i,i+1} B)$$ relate? The answer is: unless we make further assumptions, we cannot show them to be equivalent. In fact, when type theory is given with explicit $\mathsf{lift}_{i,j}$ maps, we include judgemental equalities which say "lifting maps commute with type constructions", such as, for $i < j$, $$\mathsf{lift}_{i,j}(A =_{\mathcal{U}_i} B) \equiv (\mathsf{lift}_{i,j} A =_{\mathcal{U}_{j}} \mathsf{lift}_{i,j} B).$$ These sorts of details are usually skipped in informal presentations of type theory. In particular the HoTT book is a bit sloppy on this point. (But the formalizations of HoTT in Coq, Agda and Lean are not.)

$\endgroup$
2
$\begingroup$

The induction principle for $=_{U_{i+1}}$ gives you a map $(A=_{U_{i+1}}B)\rightarrow (A=_{U_i}B)$.

In HoTT without univalence, there is no map $(A=_{U_i}B)\rightarrow (A=_{U_{i+1}}B)$: indeed, you could assume the univalence axiom only for universe $U_i$. In that case, $A\simeq B$ gives you by univalence an inhabitant of $A=_{U_i}B$, but not of $A=_{U_{i+1}}B$: with the rules of the theory, the inhabitants of the identity types $=_{U_{i+1}}$ can only take the form $refl_A$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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