Currently, the triangle identities in the definition of a unit-counit adjunction are stated as equalities of natural transformations. In this form they're a pain to state, particularly because the unit and associativity laws for functors don't hold definitionally.
Because natural transformations are equal if they're equal on objects, there's an equivalent definition that just talks about equality on objects and avoids these issues (because those laws do hold definitionally for functions). Currently there's a helper function make⊣ that goes from this simpler condition to the "real", complicated one.
But it seems to be easier overall to just use the simpler condition as the definition, so this PR makes that change. I don't think the complicated condition is particularly useful to have around, what with it being so gnarly.
ecavallo
commented
1 year ago
Currently, the triangle identities in the definition of a unit-counit adjunction are stated as equalities of natural transformations. In this form they're a pain to state, particularly because the unit and associativity laws for functors don't hold definitionally.
Because natural transformations are equal if they're equal on objects, there's an equivalent definition that just talks about equality on objects and avoids these issues (because those laws do hold definitionally for functions). Currently there's a helper function
make⊣that goes from this simpler condition to the "real", complicated one.But it seems to be easier overall to just use the simpler condition as the definition, so this PR makes that change. I don't think the complicated condition is particularly useful to have around, what with it being so gnarly.