Justifying Lean's axioms with cubical type theory

Stream: Type theory

[E M]

The major problem of Lean foundations is that it uses several axioms, namely propext, funext, quot.sound and choice.

However, propext, funext and quot.sound are trivially provable in cubical type theory, so as a thought experiment we could imagine replacing the foundation of Lean with it.

Proving the axioms would require to replace Lean's equality with path equality; the issue is that Lean has UIP, but it seems this is easily solved by adding an isSet typeclass instance hypothesis for all type parameters that requires the type to be an HoTT Set, i.e. the types for which UIP holds. AFAIK unless non-Set HITs are defined, all types that can be formed are Sets, and quotients are Set HITs by definition (the squash constructor in https://agda.github.io/cubical/Cubical.HITs.SetQuotients.Base.html), and it should thus be possible to automatically generate the isSet proofs. It also may be possible to use a two-level type theory which directly provides a sort of Sets.

As for the axiom of choice, changing the sort doesn't work because "sets with choice" are not closed under formation of function types; however, it seems that it should still be possible to define a typeclass for sets with choice and automatically relativize all Lean statements using choice to it, and recursively add whatever instances the child definitions require to the parent definitions.

So if I'm not missing something this would allow in principle to essentially translate elaborated Lean code to Cubical Agda with no axioms and having it typecheck.

This would mean that one can be more confident in Lean's consistency and also it would enable to replace Lean's foundations with cubical type theory and still keep compatibility with Lean 4 code, but also allow definitions outside it without the Set-only restriction. One could then, still keeping compatibility, gradually generalize mathlib statements to work on non-Sets where valid, and to avoid choice where unnecessary, and then have a formalization of mathematics that doesn't make any compromise.

Does this work or is there any issue in this reasoning?

[Johan Commelin]

still keep compatibility with Lean 4 code

I think this clause is doing a lot of heavy lifting.

[Luigi Massacci]

As a point of pedantry, note that functional extensionality is also a theorem in lean, see docs#funext

[Chris Bailey]

E M said:

This would mean that one can be more confident in Lean's consistency

Can you elaborate on this? I'm not sure your proposal makes progress on that front unless the axioms of cubical agda are dramatically simpler than those of Lean or Agda's kernel/implementation is somehow more trustworthy than Lean's. If you believe one or both of those to be the case, I'd be interested to know why.

[Henrik Böving]

Chris Bailey said:

E M said:

This would mean that one can be more confident in Lean's consistency

Can you elaborate on this? I'm not sure your proposal makes progress on that front unless the axioms of cubical agda are dramatically simpler than those of Lean or Agda's kernel/implementation is somehow more trustworthy than Lean's. If you believe one or both of those to be the case, I'd be interested to know why.

I would say that cubical type theory is even more complex, they buy into a lot of additional inference rules around the whole cube thing in order to build up the theory.

[Matthew Ballard]

/me is resisting time cube jokes

[Henrik Böving]

(deleted)

[Matthew Ballard]

But seriously, I think a main selling point of Lean is the flexibility of its metaprogramming. At a minimum, a cubical TT DSL would be very cool.

[Matthew Ballard]

I don't see why Lean can't have all the type theories (just not in the kernel)

[Andrés Goens]

Matthew Ballard said:

But seriously, I think a main selling point of Lean is the flexibility of its metaprogramming. At a minimum, a cubical TT DSL would be very cool.

wouldn't that require it be the other way around? i.e. embedding cubical TT into Lean's TT? (sounds more complicated/unclear if feasible as a shallow embedding)

[Matthew Ballard]

Sure, but that is what I find most interesting

[Mario Carneiro]

Henrik Böving said:

Chris Bailey said:

E M said:

This would mean that one can be more confident in Lean's consistency

Can you elaborate on this? I'm not sure your proposal makes progress on that front unless the axioms of cubical agda are dramatically simpler than those of Lean or Agda's kernel/implementation is somehow more trustworthy than Lean's. If you believe one or both of those to be the case, I'd be interested to know why.

I would say that cubical type theory is even more complex, they buy into a lot of additional inference rules around the whole cube thing in order to build up the theory.

I would go further and say that cubical type theory is the most complex axiomatic system I have ever seen presented. It's also not just one thing, there are many versions of CTT (I know at least 5), which makes it difficult as an implementer to make CTT theorists happy AFAICT. That said, I am all in favor of any attempt to embed theory X in theory Y since we learn a little bit about X and Y every time we try it

[Kyod]

Maybe a bit late to chime in but if you want to build a model of lean in another theory then XTT might be a well-suited by product of cubical type theories for that end because XTT is already specialized to talk about (homotopy) sets (technically 0-truncated types in HoTT linguo). There is also a related line of work on Observational Type Theories (orginal OTT paper) whose metatheory (including normalization and canonicity) has been established in a recent series of papers (here, tackling impredicativity and inductives). However all these papers are targetting other properties than (relative) consistency that can be established through a model to sets (assuming a metatheory that's strong enough).