For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.
The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...
*) I'm going by second hand accounts here, please correct me if you think this statement is too strong.
The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...
*) I'm going by second hand accounts here, please correct me if you think this statement is too strong.