For readers who aren&#x27;t already familiar with this, I&#x27;ll note that this is in large part what Homotopy Type Theory is about making easy to work with. <a href="http:&#x2F;&#x2F;homotopytypetheory.org&#x2F;book&#x2F;" rel="nofollow">http:&#x2F;&#x2F;homotopytypetheory.org&#x2F;book&#x2F;</a> is a good introduction.