[foxyseta]

Description

Closes #625. As per #625 (comment), I proved that the universe of h-sets is no h-set. However, the construction is currently not parametric in a universe level, because Data.Bool is not.

After I am done here, I would like to move on to proving that the universe of h-1-groupoids is no h-1-groupoid, using the circle as a counterexample.

I am having trouble with nix run --experimental-features nix-command -f . sort-imports src/1Lab/Counterexamples/HLevel/Universes.lagda.md. I get:

sort-imports: src/1Lab/Counterexamples/HLevel/Universes.lagda.md: hGetContents: invalid argument (cannot decode byte sequence starting from 226)
HasCallStack backtrace:
  collectBacktraces, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:169:13 in ghc-internal:GHC.Internal.Exception
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/IO.hs:260:11 in ghc-internal:GHC.Internal.IO
  throwIO, called at libraries/ghc-internal/src/GHC/Internal/IO/Exception.hs:315:19 in ghc-internal:GHC.Internal.IO.Exception
  ioException, called at libraries/ghc-internal/src/GHC/Internal/IO/Exception.hs:319:20 in ghc-internal:GHC.Internal.IO.Exception

EDIT: A maintainer helped me fix this in this thread!

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[ncfavier]

hGetContents: invalid argument (cannot decode byte sequence starting from 226)

This usually means that you are not using a UTF-8 locale. What's your platform? Does export LC_ALL=C.UTF-8 fix it?

However, the construction is currently not parametric in a universe level, because Data.Bool is not.

You could Lift it.

[Lavenza]

Pull request preview

New pages

• 1Lab.Counterexamples.HLevel.Universes (+206, -0)

Changed pages

• HoTT (+3, -0)

[foxyseta]

This usually means that you are not using a UTF-8 locale. What's your platform? Does export LC_ALL=C.UTF-8 fix it?

Thanks, that fixed it. I am on Alpine.

You could Lift it.

Implemented in a830551! I was worried it would make everything much uglier, but it doesn't seem all that bad.

Shall I move on to h-groupoids?

[foxyseta]

Sorry, I'll actually try to build the 1lab locally before fixing the link this time.

[foxyseta]

✅ Build succeeded in 17m33s
buildPhase completed in 17 minutes 44 seconds

I also had a look on localhost. Is there a recommended grammar style for citations? Right now, I am writing stuff like

• In example 3.1.9, (2013) uses ...
• Our proof follows section §2 of (2024).
• In the absence of these, (2015) explains...

which is probably not want you want me to do.

[plt-amy]

✅ Build succeeded in 17m33s

you might want to 1lab-shake -j, that build time seems excessive

[foxyseta]

Man burst into tears, says "But doctor, my 1lab-shake is -j 🥲". I am using Nix, and default.nix seems to always 1lab-shake -j, correct? Is my hardware just too low-spec? I am on 8GBs of RAM, Intel Core i5-6200U CPU @ 2.30GHz.

After having a look at "On symmetries of spheres in univalent foundations", it seems that $n = 3$ will require Gottlieb’s theorem. Should I open a different PR? Which module does each of the following belong to?

• Definition of a fibre for pointed types;
• Gottlieb’s Theorem from classical homotopy theory. It needs the following two:
• for any group $G$, there is a pointed equivalence between (1) the delooping of $G$'s center and (2) the loop space of the universe pointed at the delooping of $G$;
• for any group $G$, there is a pointed equivalence between (1) the set-truncated loop space of the universe pointed at the delooping of $G$ and (2) the outer automorphisms of $G$.

[ncfavier]

I was thinking it should be possible to show $$(S^1 = S^1) = S^1 + S^1$$ directly without all the general machinery the paper develops, but I admit I haven't thought about it very carefully. Maybe the theory of degrees of maps of spheres can help.

It should definitely be possible to prove directly that $$S^1 = S^1$$ isn't a set though, since we already know that the identity $$S^1 \to S^1$$ has a nontrivial loop (always-loop).

It's up to you how far you want to take this.

[foxyseta]

It should definitely be possible to prove directly that $S 1 = S 1$ isn't a set though

You are right. I proved it directly. Lifting the circle resulted in a bunch of duplicated code though...
Because $S^1$ and $\text{Lift}\ \ell\ S^1$ live, in general, in distinct universes, I guess I can't use univalence to turn $\text{Lift-}\simeq$ into an equality, which means I cannot just apply subst to an arbitrary theorem proven for the unlifted circle. is there some other strategy I was supposed to use to avoid duplicated code?

Coincidentally, is there a reason why the circle in the 1lab is currently not parametric in a universe level?

[ncfavier]

You could show that the lowest universe of groupoids is not a groupoid using S¹, then stick Lift-is-embedding and embedding→is-hlevel together to extend the result to larger universes (the same applies for Bool and sets).

Coincidentally, is there a reason why the circle in the 1lab is currently not parametric in a universe level?

Making it parametric in a level would probably require adding explicit levels in a bunch of places.

[foxyseta]

Lift is an embedding between type universes, and not between $3-Type_0$ and $3-Type_\ell$, though. I would then have to show that it restricts to the latter, right?

[ncfavier]

Yes

[foxyseta]

I gave it a (partial) try, but it increased the lines of code by quite a bit, so I am personally content with the current status of the PR.

Making it parametric in a level would probably require adding explicit levels in a bunch of places.

Yeah, fuzzy finding for import.*Circle returns 17 results. It doesn't sound like exciting work, but I could take it on at a later time, if you need help with it, making the code currently using $S^1$ parametric, too.