A totally ordered set is a set equipped with a total order. Internally in a topos, weak totality does not imply decidable equality. The empty ordered set is allowed unless an inhabitation axiom is explicitly imposed.
New to topics? Read the docs here!