Axioms

Stream: Infinity-Cosmos

[Jason Rute]

Silly question: Does the theory of infinity categories go through in Lean’s usual axioms (including choice), or does one need to assume something like higher cardinals (higher than those already in Lean). (I clearly don’t know exactly what an infinity category is exactly. I could easily imagine it could be be defined in ZFC, or even PA. I could also just as easily imagine having an infinity category would allow you to construct a model of Lean’s type theory.)

[Johan Commelin]

This project shouldn't need any additional axioms beyond the standard 3. Whether some standard axioms can be avoided is something I don't know anything about.

[Mario Carneiro]

Not sure how helpful this is, but: the "infinity" in infinity categories is an independent degree of freedom from the universe hierarchy. I have seen people draw it as a 2D plane. In HoTT, each universe can have an independent "amount" of univalence, e.g. Type 0 is a 1-type, Type 1 is a 42-type, Type 2 is a 37-type and the others are infty-types for example. All of these variations have the same consistency strength, it is only the number and closure properties of universes that matters for consistency.