Finite strict total orders and increasing injections, including the empty order, give a presheaf classifier for strict total orders. Trichotomy locally merges two finite sorted tuples, identifying equal entries. A strict map from a chain is injective, so parallel maps admitting the same realization are already equal. Reflexification gives a geometric morphism to the classifying topos of linear orders; pulling back weak totality gives exactly strict trichotomy.
Articles by others on the same topic
There are currently no matching articles.