Are you talking along the lines of the red family of provers?
What makes the cubical approach more powerful? What makes lean weak?
What makes the cubical approach more powerful? What makes lean weak?
Lean is not weak, it just commits to something called Uniqueness of Identity Proofs (UIP). This is inconsistent with Univalence, a property that cubical type theories have. Necessarily, neither system can express "all of math." So it goes.
Leo chose UIP to get a novel way to get really powerful automation of equality proofs. Leo is very, very good at this; this is his whole shindig. But he had to hack around things a bit in order to get what he wanted. The paper by Bas and his student shows that in cubical, you don't have to hack around things; this automation of equality proofs arises in the natural way.
The gap is not fundamental, and it irritates me when it is attributed to the choice of UIP. The reason Lean is so useful is because the people working on it are good at building automation. The people working on cubical are much more interested in foundations. We need people who are interested in automating cubical; once we get that, the proof assistant that arises from it will be better than anything we have ever seen.
Same here.
But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.