book icon indicating copy to clipboard operation
book copied to clipboard

max and sup

Open ncfavier opened this issue 7 months ago • 9 comments

Some people are complaining that the HoTT book uses $\mathsf{max}(x, y)$ to denote the $\mathsf{sup}$ operation in a lattice, and in particular the $\mathsf{sup}$ of two real numbers, whereas in traditional mathematical practice $\mathsf{max}\{x, y\}$ denotes the maximum of the set $\{x, y\}$, i.e. the $\mathsf{sup}$ with the added side condition that $\mathsf{max}\{x, y\} \in \{x, y\}$.

Is there a reason for this apparent departure from convention? Was it to avoid conflict with the $\mathsf{sup}$ constructor for $W$-types or the $\lor$ logical connective?

ncfavier avatar Jul 13 '24 09:07 ncfavier