(0,1)-category

(0,1)-topos

# Contents

## Idea

A strict total order which is not a connected relation.

## Definition

A strict weak order is a strict preorder which is also a cotransitive relation.

These are sometimes called strict partial orders in the literature, but the term “strict partial order” is also used for other order relations in mathematics.

Strict weak orders are used in models of the real numbers which have infinitesimals, such as in the smooth real numbers in synthetic differential geometry, and thus where not every real number not greater than or less than zero is equal to zero.

## Properties

###### Theorem

Strict weak orders are asymmetric relations.

###### Proof

Transitivity of $\lt$ says that for all $x \in S$ and $y \in S$, $x \lt y$ and $y \lt x$ implies $x \lt x$. However, irreflexivity says that for all $x$, $x \leq x$ is always false. This implies that for all $x$ and $y$, $x \lt y$ and $y \lt x$ is always false, which is precisely the condition of asymmetry.

###### Theorem

Connected strict weak orders are pseudo-orders.

###### Proof

The proof is the same as above, except both relevant orders are connected relations.

### Preorder of a strict weak order

An important part of a strict weak order is that it is a preorder.

###### Theorem

The negation of a strict weak order is transitive.

###### Proof

The contrapositive of cotransitivity says that

for all $x$, $y$, and $z$, if $x \lt y$ or $y \lt z$ is false, then $x \lt z$ is false.

By one of de Morgan's laws, that $x \lt y$ or $y \lt z$ is false is logically to equivalent to that $\neg(x \lt y)$ and $\neg(y \lt z)$, and substituting this into the original statement results in

if $\neg(x \lt y)$ and $\neg(y \lt z)$, then $\neg(x \lt z)$

which is precisely transitivity for the negation of the strict weak order.

###### Theorem

The negation of a strict weak order is reflexive.

###### Proof

Irreflexivity states that $\neg (x \lt x)$ is true, which is precisely reflexivity for the negation of the strict weak order.

###### Theorem

The negation of a strict weak order is a preorder.

###### Corollary

The incomparability relation of a strict weak order, $\neg (x \lt y) \wedge \neg (y \lt x)$, is an equivalence relation

###### Proof

For every preorder, $(x \leq y) \wedge (y \leq x)$ is an equivalence relation. Since $\neg (x \lt y)$ is a preorder, $\neg (x \lt y) \wedge \neg (y \lt x)$ is an equivalence relation.

• Auke Booij, Analysis in univalent type theory (2020) $[$etheses:10411, pdf$]$