Total Ordering

Given a set $A$, a Partial Order $\le :A\text{texttimes}A\to \mathrm{Type}$. We say that $\le$ is a total ordering exactly when for every pair of $x,y:A$, Either $x\le y$ or $y\le x$.