Classifying topos of strict linear orders

ID: classifying-topos-of-strict-linear-orders

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.

New to topics? Read the docs here!