Commit 2023-10-25 10:47 f81eaba3

refactor: Move the data fields of MonoidalCategory into a Struct class (#7279) This matches the approach for CategoryStruct, and allows us to use the notation within MonoidalCategory. It also makes it easier to induce the lawful structure along a faithful functor, as again it means by the time we are providing the proof fields, the notation is already available. This also eliminates tensorUnit vs tensorUnit', adding a custom pretty-printer to provide the unprimed version with appropriate notation.