All Questions
Tagged with cubical-type-theory proof-search
1
question
9
votes
2
answers
590
views
What is the state of the art in proof automation in HoTT/CuTT?
One of the frequent criticisms of HoTT is that it requires a lot of lemmata keeping track of which types are sets/propositions etc. And a frequent counterpoint is "It can be automated."
...
- 4,025