@programming_discussions oh cool. I saw something like this a while back implemented as a Python library somewhere in the astropy universe. I'm curious how to manage the type checker when considering "unexpectedly" equivalent types. Eg, conservation laws or einsteins equation (with and without momentum). Also, if the notion of an infinitesimal can/should be captured as a type.