We explicitly require that equalities of morphisms be hProps.  So long as we assume functional extensionality, `identity_identity` is provably equal to both `right_identity` and `left_identity`.