agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard
verified publisher icon agda

Create `HasBraidedInterchange` and `HasSymmetricInterchange` .

Open JacquesCarette opened this issue 4 years ago • 0 comments

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.

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

JacquesCarette avatar Aug 13 '21 03:08 JacquesCarette