Open JacquesCarette opened 3 years ago
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?
Kelly
σ⁻¹-coherence
_Originally posted by @sstucki in https://github.com/agda/agda-categories/pull/294#discussion_r687802566_
Maybe we should just move all of those one-line
Kellyvariants 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_