Explain Homotopy type theory like I'm five
As the title, I'm looking for a clear overview summary of HOTT.
Tags: explainlikeimfive