Post #2538505

One of the biggest realizations we had about Cubical Agda is that the cubical Path type is not a *replacement* of the inductive Identity type, but instead *complementary* to it. The reason being that they have very different definitional behavior. An intuition for why is that the inductive Identity type is defined by a left adjoint universal property whereas the Path type is defined by a right adjoint universal property. This means that the inductive Identity type works well when we are mapping out of it: i.e. when we want to use J. This means that often when you want to *abstract over* a *definitional* equality then you should use the inductive Identity type because a definitional equality will be refl and so the abstraction will reduce to the exact thing you started with. This is not the case for the Path type because you will end up with a transport refl, which doesn't typically reduce. On the other hand, by nature of being a right adjoint type, the Path type has a definitional eta equality (just like products and functions). This makes it so that a Path in a product type is not just isomorphic to paths between the projections but that this Isomorphism is a *definitional* equality. This is not the case for the inductive Identity type, which doesn't have definitional eta because it's inductive (same for sums/empty). There the Isomorphism between Identity at a product type and pair of identity proofs is not definitional because the round trip will be stuck pattern matching on the original equality. So we have found that in certain spots in the library it is essential to use inductive equality to avoid large blowup of goals or unnecessary transports when abstracting over things. On the other hand we have at least one spot where it was essential to use Path to get some definitional equalities to hold for structures that contained equality proofs in them.