Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: Identity type in lower universe?

finegeometer (Jun 21 2023 at 13:14):

In HoTT, would it be consistent for the identity type $a =_A b$ to always live one universe below $A$?

For many types, this works already:

• $U_n : U_{n+1}$. But $X =_{U_n} Y$ is equivalent to $(f : X \to Y) \times ((y : Y) \to \mathrm{isContr}(\mathrm{fiber}(f)))$, so we can certainly put it in $U_n$.
• Let $A : U_n, B : A \to U_n$. Then $(a_1,b_1) =_{(a : A) \times B(a)} (a_2,b_2)$ is equivalent to $(p : a_1 =_A a_2) \times subst(B,p,b_1) =_{B(a_2)} b_2$. So if $A$ and $B$ have identity types in $U_{n-1}$, so can $(a : A) \times B(a)$.
• et cetera.

But this doesn't automatically work for function types. Let $A : U_n$ and $B : A \to U_n$. Then $f =_{(a : A) \to B(a)} g$ is equivalent to $(a : A) \to f(a) =_{B(a)} g(a)$. But even if $A$ and $B$ have identity types in $U_{n-1}$, this still lives in $U_n$.

This would work if the universes were impredicative. But then again, nested impredicative universes are inconsistent anyway, or so I've heard.

Tom de Jong (Jun 21 2023 at 13:22):

I imagine it's possible to construct a counterexample to this, e.g. by a higher inductive type with a point and a loop at the point for every element of a universe $\mathcal U_n$. But I'm not sure.

Ben Logsdon (Jun 22 2023 at 14:49):

This feels impossible to me. However, there is a weaker version of it which is possible. If we assume propositional resizing (see the end of Section 3.5 of the HoTT book), then every mere proposition is equivalent to a mere proposition in the bottom universe. Therefore, for any type which happens to be a set, its identity types will all be equivalent to types at the bottom universe (again, assuming propositional resizing).

Ben Logsdon (Jun 22 2023 at 14:54):

Elaborating on @Tom de Jong's idea, I think we can construct a counterexample as follows.

Assume that we have enough higher inductive types to construct suspensions of arbitrary types, and that constructing the suspension does not raise the universe level. (See HoTT book section 6.5 for the definition of suspension.) Thus, if $A : \mathcal{U}_i$, then $\Sigma A : \mathcal{U}_i$. Let $A : \mathcal{U}_i$ be a type which is not equivalent to any type in $\mathcal{U}_{i-1}$. Then $\Sigma A$ is a type in $\mathcal{U}_i$, but its path type $N =_{\Sigma A} S$ is equivalent to $A$, therefore it is not equivalent to any type in $\mathcal{U}_{i-1}$ since $A$ isn't.

EDIT: @Tom de Jong Pointed out that this is not correct. Thanks!

Tom de Jong (Jun 22 2023 at 17:48):

@Ben Logsdon It's not true that $N =_{\Sigma A} S$ is equivalent to $A$. E.g., if $A$ has decidable equality, then we can characterise $\pi_1(\Sigma A)$ as the type of certain lists of elements of $A$.

Mike Shulman (Jun 22 2023 at 18:26):

However, you can do some related things. With HITs we can also construct Eilenberg-MacLane spaces: for any set (i.e. 0-type) $G$ with a group structure, there is a type $BG$ with a point $\star$ such that $\star =_{BG} \star$ is equivalent to $G$. So we will have a counterexample as soon as there is a group in $\mathcal{U}_i$ that is not equivalent to any type in $\mathcal{U}_{i-1}$. The first such $G$ that occurs to me is the surreal numbers under addition, but probably there is a simpler one.

Tom de Jong (Jun 22 2023 at 18:36):

Thanks @Mike Shulman. There is work by @Martín Hötzel Escardó with Marc Bezem, Thierry Coquand and Peter Dybjer where they show:

For any universe 𝓤, there is a group in the successor universe 𝓤⁺ which is not isomorphic to any group in 𝓤.

https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.FreeOverLargeLocallySmallSet.html

Tom de Jong (Jun 22 2023 at 18:39):

Specifically, they show: if there is a large, locally small set, then there is a large group. We can then instantiate this with the large, locally small set of ordinals.

John Baez (Jun 22 2023 at 19:15):

This is the first time I've seen anyone mention the Eilenberg-Mac Lane space of the surreal numbers!