Now that equality has become computationally relevant but composition of equality remains cumbersome, the statement of various equality laws in the cubical library feels "wrong". Here I want to explore an alternative approach.
To avoid confusion, I want to start by emphasizing what I'm not proposing.