Author Archives: Carlo Angiuli

HoTT in prose

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

Posted in Uncategorized | 13 Comments