Author Archives: Carlo Angiuli

I have adapted some basic HoTT theorems and proofs to prose form, in an attempt to better understand the results and their proofs. The Coq proof scripts often obscure details of the exposition, like the choice of fibration in an induction tactic, … Continue reading →