## Franklin's Notes

### Order type

An order type is (somewhat non-rigorously?) defined as an equivalence class of ordered sets, where order-equivalence is defined by order isomorphism, i.e. $A\sim B$ if there exists an order-preserving bijection $f:A\to B$. Alternatively, we can define a category of order types, denoted $\mathsf{OrdType}$, as the skeleton of the category $\mathsf{LinOrd}$, so that $\mathsf{OrdType}=\mathrm{sk}(\mathsf{LinOrd})$.