More WIP

Next step is to give versions of the lemmas for rewrite for the
inverses, and then do the same munging we did in the Grothendieck
construction here, for speed, to prove the identity laws.