definition of adjunctions using the triangle identities

Stream: new members

[Dean Young]

Can someone direct me to where math lib has the definition of adjunctions using the triangle identities?

[Notification Bot]

A message was moved here from #new members > Mention Lean 4 somewhere in the Lean Community pages by Eric Wieser.

[Eric Wieser]

I can direct you to a better place to ask that kind of question; i.e., not in an unrelated Zulip topic :wink:

[Adam Topaz]

docs4#CategoryTheory.Adjunction.mkOfUnitCounit

[Scott Morrison]

Just pinging @Kind Bubble so they find this message after the move. :-)