The universe of n-types is not an n-type

[ncfavier]

While showing that Set ℓ is not a set is straightforward (example 3.1.9 in the HoTT book), showing that n-Type ℓ n does not have hlevel n is somewhat more involved: see Higher Homotopies in a Hierarchy of Univalent Universes.

Formalising this could be a good first issue for someone looking to contribute.

[alicelaroche]

It doesn't think the paper you shared shows that n-Type ℓ n does not have hlevel n , if it understands correctly it shows that n-Type (n+ℓ) n does not have hlevel n.

As far as it knows, your claim is an open problem and the people it discussed with about it tend to think it is either undecidable or false.

[ncfavier]

You're right, sorry! That this is thought to be undecidable or false is surprising to me, though. In the presence of HITs, it feels like it should at least be possible to prove that the type of groupoids in U₀ (n-Type lzero 3) is not a groupoid, by adequately resizing whatever construction that paper uses? Is this really not possible?

(Without HITs, it's possible to model the universe hierarchy so that the nth universe contains only n-types, so in that case it's consistent that U₀ is a groupoid.)

(P.S.: I opened this because in this module I refuted a strong version of "sets cover" by deriving ∀ {ℓ} → is-groupoid (n-Type ℓ 3) from it, so showing that ¬ is-groupoid (n-Type 3 3) would suffice to derive a contradiction.)

[ncfavier]

At least for groupoids, the paper on symmetries of spheres shows that S¹ ≡ S¹ is not a set, which implies that no universe containing S¹ can be a groupoid.

[alicelaroche]

Yes you're right sorry, it was thinking in the absence of HITs. With HITs it sounds possible but hard.
With HITs it sounds more plausible to show your claim.

[ncfavier]

Your point remains that this is harder than I thought. I asked elsewhere and it looks like it should be possible (in theory...) to prove the general result via Eilenberg–MacLane spaces.

Let's say the "good first issue" here would be to show that universes of sets are not sets (via Bool) and that universes of groupoids are not groupoids (via S¹).

[alicelaroche]

Where should that live ? It thought 1LAb.HLevel.Universes would be the most obvious place, but then you get a circular reference when importing Bool and S¹

[ncfavier]

Maybe 1Lab.Counterexamples.HLevel.Universes or something.