HoTT in Lean

Stream: general

[Reid Barton]

@Ulrik Buchholtz I was wondering if you could elaborate a bit on the project you suggested during one of the Lean Together discussions. I didn't quite follow the kind of setup you have in mind.

[Ulrik Buchholtz]

Ulrik Buchholtz I was wondering if you could elaborate a bit on the project you suggested during one of the Lean Together discussions. I didn't quite follow the kind of setup you have in mind.

It's not a fully elaborated idea yet, but very roughly, the idea is to work in simplicial sets (or perhaps cubical sets) as a 1-topos model of extensional type theory. There we have meta-propositions and meta-type universes that we can compute with. Then we axiomatize the homotopical structure: the univalent universes of fibrant types closed under homotopy pushouts. This idea has traces to Voevodsky's HTS, but the new developments in Two-Level Type Theory and Applications, Coquand's Universe of Bishop Sets, as well as Definitional Proof-Irrelevance without K make me hopeful that we can devise rules for specialized univeses of strict propositions (inside the meta-propositions) and strict or Bishop sets mapping to the meta-sets such that these are equivalent to the homotopy propositions and sets, respectively, and with rules for inductive types in these universes with appropriate eliminators, and that all this can be made seamless with metaprogramming. For any type $A$ with points $a, b : A$, we have both an identity type $a =_A b$ (representing identifications/paths) as well as a meta-equality type $a=_A^m b$ that is a meta-prop representing equality of cells. There are many possible variations (e.g., using Orton-Pitts style definitions of fibrancy structures in cubical sets), but I was thinking that if we don't care about constructivity, then a relatively simple setup would suffice.

[Reid Barton]

So is this similar to the setup used in https://github.com/annenkov/two-level?
In particular the intended interpretation of the outer Type is supposed to be a simplicial set, so we cannot use classical reasoning in the outer level, right?
One thing I could not work out is whether we ever add any constants which reinforce the interpretation of Type as specifically simplicial sets, as opposed to any model topos (say) with the expected conditions of fibrancy of sums, fibrant universes, univalent universes etc.

[Reid Barton]

How would this approach compare to working in the "standard" model where a Type is a set, and defining the internal version of Type to be a simplicial set in the classical sense, and simply proving (okay, it is not so easy, but I also think it's not out of reach) theorems about fibrancy of sums and universes and so on?
Basically my question is: if we had all the model category-theoretic prerequisites for the "model theory" of HoTT in place, how easy would it be to build an "internal HoTT system" that is usable in practice? Would it differ substantially from the approach you are suggesting?

[Ulrik Buchholtz]

So is this similar to the setup used in https://github.com/annenkov/two-level?

Yes, Danil Annenkov is a co-author of the two-level type theory paper.

So we cannot use classical reasoning in the outer level, right?

Not directly, no, but the way I was thinking about it, the outer (meta) level is an “implementation detail” and shouldn't be used for reasoning. So you add axioms about the (univalent, inner) types, but not about the meta-types. That said, with a 1-cohesive modality, you could capture the outermost 1-topos Set that simplicial sets sits 1-cohesively over, and add axioms for that, but that seems unnecessary.

One thing I could not work out is whether we ever add any constants which reinforce the interpretation of Type as specifically simplicial sets, as opposed to any model topos (say) with the expected conditions of fibrancy of sums, fibrant universes, univalent universes etc.

Well, we'd add axioms that the inner higher topos has choice, Reedy-limits, Whitehead's principle and sets cover. That should narrow down the Grothendieck $(\infty,1)$-topos models considerably. We could then further add that geometric realization of simplicial sets is surjective.

[Ulrik Buchholtz]

How would this approach compare to working in the "standard" model where a Type is a set, and defining the internal version of Type to be a simplicial set in the classical sense, and simply proving (okay, it is not so easy, but I also think it's not out of reach) theorems about fibrancy of sums and universes and so on?
Basically my question is: if we had all the model category-theoretic prerequisites for the "model theory" of HoTT in place, how easy would it be to build an "internal HoTT system" that is usable in practice? Would it differ substantially from the approach you are suggesting?

My guess is that with current technology, it would be much more cumbersome. My hope was that with a little macroprogramming in Lean4, you could reuse most of mathlib as is, but in the univalent layer. A slight price to pay is that there are two (mathematical) prop universes, one strict, and one homotopical, but they would be equivalent (and both equivalent to bool). I fear that the (shallow/deep?) embedding approach would not be nearly as transparent in practice.
But (as I mentioned last week), I would actually love to be wrong, because I'd like to see many applications of internal languages (for different kinds of categories or first-order models or …) be transparent and easy to use.