I'm now tempted to add two more records: HasBraidedInterchange and HasSymmetricInterchange with the extra fields that are in the respective modules. This would completely separate the axioms from the proofs, so that the former could be used in down-stream proofs/constructions without pulling in the big concrete proof terms. But maybe this is for a future PR.
I'm now tempted to add two more records:
HasBraidedInterchangeandHasSymmetricInterchangewith the extra fields that are in the respective modules. This would completely separate the axioms from the proofs, so that the former could be used in down-stream proofs/constructions without pulling in the big concrete proof terms. But maybe this is for a future PR._Originally posted by @sstucki in https://github.com/agda/agda-categories/pull/294#discussion_r687787854_