Move all one-line`Kelly` variants into the module where the original properties are proved?

[JacquesCarette]

Maybe we should just move all of those one-lineKelly variants into the module where the original properties are proved? They would probably be more useful there? And similarly for σ⁻¹-coherence?

Originally posted by @sstucki in https://github.com/agda/agda-categories/pull/294#discussion_r687802566