Added groupoid laws for identity types.
Trying to understand proof of having all paths implying being in hProp.