We now use equalities between pointed homotopies in the library. However, this almost always requires function extensionality, which doesn't compute. We have redefined pointed homotopies as a special case of a dependent pointed map, so we can construct pointed homotopies between pointed homotopies, which doesn't require function extensionality.
We now use equalities between pointed homotopies in the library. However, this almost always requires function extensionality, which doesn't compute. We have redefined pointed homotopies as a special case of a dependent pointed map, so we can construct pointed homotopies between pointed homotopies, which doesn't require function extensionality.
This also means we should redefine
phsquare.