https://github.com/agda/agda-stdlib/blob/b0505d661fbbfecf7ffeae20cc4b48c8ef41e078/doc/README/Design/Hierarchies.agda#L301 It should be containing operations but not laws, right?