A lawyer, a doctor, and a type theorist are discussing whether it is better to have a lover or a spouse. The lawyer says, “Clearly it is better to have a lover - for reasons I need not explain.” The doctor says, “No, no, it is better to have a spouse - for reasons I need not explain.” The type theorist says “You’re both wrong! It’s clearly better to have both a lover and a spouse: then when the spouse thinks you’re with the lover, and the lover thinks you’re with the spouse, you can be in your office proving theorems.”

(I hope there are no type theorists in the audience…)