I was making this little table of analogies in my thesis with all the usual stuff
| Substitution | Identity |
| β-reduction | η-expansion |
| Soundness | Completeness |
| Cut Elimination | Self-Entailment |
| Local Reduction | Local Expansion |
and I noticed that I associate everything in the left column with dark value and blue hue, and everything in the right column with light value and yellow hue. Also, in adjunctions the right adjoint F is unquestionably deep red-orange, and the left adjoint U is light gray-blue.. Do any of you other logic/types/λ-calculus people have any color or other informal associations with the left-right distinction in this table?
As formally spurious as they are, I sometimes think these strong, almost tangible intuitive feelings about formal concepts are essential parts of a sort of hashing algorithm going on in my brain without which I would not as easily be able to remember and manipulate the concepts in question.
