Project: Brunerie infinity-groupoids

Stream: maths

[Paul Reichert]

Hi, I just wanted to let you know that I have started a little side project about infinity-groupoids. It is in an early stage, but I wanted to share my thoughts in case someone else is interested in it. (Happy to move to GitHub if someone wants to collaborate.)

What/Why?

In the long run, I'd like to formalize HoTT-style proofs in Lean -- dodging univalent foundations by working with infinity-groupoids instead of HoTT types, functors between them instead of HoTT functions and equivalences instead of HoTT equality. As far as I can tell, it's totally open how well it will work out -- my motivation is curiosity in the design space and the prospect to learn some infinity-category theory on the way. I'm neither an expert in infinity-category theory nor in HoTT.

But the first step is to even have a notion of infinity-groupoid, and that's what I'm working on right now.

How?

As I am less excited about working formally with Kan complexes than with Guillaume Brunerie's more algebraic definition, I am going with the latter.

I find Brunerie infinity-groupoids very beautiful. Being based on globular sets, they are conceptually closer to a type theory than Kan complexes, and they provide a nicely motivated, unified account of identity paths, inverses, compositions and coherences.

This is the rough and somewhat ambitious action plan:

1. Formalize Brunerie type theory (the type theory that tells us what coherences we need).
2. Define a weak infinity-groupoid roughly as a model of this type theory.
3. Construct path spaces: The paths between two objects of an infinity-groupoid are infinity-groupoids themselves.
4. Define weak functors and construct the infinity-groupoid of weak functors between two given infinity-groupoids.
5. Define the infinity-groupoid Space.{u + 1} of (small) infinity-groupoids.
6. Construct Pi types, the J eliminator and more of the standard stuff.
7. (Stretch goal:) Implement tactics analogous to rw, simp and cases that work with equivalence instead of equality.

What's the current state?

Right now, I'm still streetfighting my way through (1.) without much prior knowledge of type theory formalization. It's fun and I learn a lot, but there are lots of tricky inductions to make and it's much more work than I expected for such a simple type theory.

There is prior work w.r.t. finishing (2.) in Agda, but I don't know whether (3.) will ever be finished in this project.

[Robert Maxton]

Just to check, you do know about the #Infinity-Cosmos project, right?

[Robert Maxton]

at any rate, it does look quite interesting, and I'd personally love to see more HoTT stuff in Lean!

[Paul Reichert]

I do, and I think it's a great project! I'm using a more elementary and limited approach. Brunerie's definition can't easily be generalized to infinity-categories, grouipoids are all I'm after. So I don't mean to compete with the infinity cosmos project (and would not be able to given the enormous amount of categorical expertise present there).