For readers who aren't already familiar with this, I'll note that this is in large part what Homotopy Type Theory is about making easy to work with. http://homo

For readers who aren't already familiar with this, I'll note that this is in large part what Homotopy Type Theory is about making easy to work with. http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/ is a good introduction.