Definition 2.16, definition 2.24, and the footnote of section 5.6 each define "total order" in different, and incompatible, ways. Several section 2.5 propositions, and one example, are also affected by the incompatible definitions. It appears that definition 2.16 is the intended (and conventional) definition of a total order. Is this correct?
If so, I can send a pull request with suggested changes to resolve the issue.
Update 6/7/23: I went ahead and sent a pull request with suggested changes to resolve this issue.
Definition 2.16, definition 2.24, and the footnote of section 5.6 each define "total order" in different, and incompatible, ways. Several section 2.5 propositions, and one example, are also affected by the incompatible definitions. It appears that definition 2.16 is the intended (and conventional) definition of a total order. Is this correct?
If so, I can send a pull request with suggested changes to resolve the issue.
Update 6/7/23: I went ahead and sent a pull request with suggested changes to resolve this issue.