name the adjunction, not its components
We give independent names to the right and the left sides of an adjunction. One of the names is usually good (Strings, Lists, Maybe, …) and one of the names is uninformative (Forget, Underlying, …).
However, each side of an adjunction determines the other. The name of any of them could well be the name of the adjunction. If we name the adjunction and not its components, we can recover its components by asking for the left or right adjoint.
- Instead of saying that the (List ⊣ Forget) adjunction is formed by a left adjoint List : Set -> Group and a right adjoint Forget : Group -> Set; we can say that the List adjunction is formed by the left adjoint List•: Set -> Group and the right adjoint List∘: Group -> Set.
Tags: adjunction, notation