Closed emilyriehl closed 1 year ago
Looks great! I would only suggest to change ladj
and radj
into left-adj
and right-adj
everywhere.
@fizruk it looks like I can't review my own pull request. The new commit just makes the requested notation change.
I started defining some of the adjunction data enumerated in #26. I'm pushing now so that this can be used for the development of limits and colimits (which is underway). There's a lot of work still to be done!
I attempted to follow the naming conventions of the style guide but would appreciate a second opinion.
As auxiliary functions I also
The Gray-interchanger is a commutative square, built by gluing two hom2 terms together. I refer to one of these as "left" and the other as "right" for lack of obvious better names.