In the canonical definition of CCCs, the field curry-resp-≈ is redundant and can be defined as a function in the record. I personally cannot see a reason justifying the redundancy but it might be there to improve definitional equality in some way (similar to introducing the redundant sym-assoc as opposed to a function using assoc), in which case there possibly needs to be a comment nearby explaining such reason.
In the canonical definition of CCCs, the field
curry-resp-≈
is redundant and can be defined as a function in the record. I personally cannot see a reason justifying the redundancy but it might be there to improve definitional equality in some way (similar to introducing the redundantsym-assoc
as opposed to a function usingassoc
), in which case there possibly needs to be a comment nearby explaining such reason.