Classifying topos of linear orders

ID: classifying-topos-of-linear-orders

With empty objects allowed, finite totally ordered sets and all weak order-preserving functions give a presheaf classifier for weak total orders. Finite tuples in a model can locally be merged into a sorted tuple using finitely many totality disjunctions. Equalizing two maps between finite chains amounts to collapsing the convex intervals forced equal. These two constructions give the flatness conditions without assuming decidable equality.

New to topics? Read the docs here!