Reference. Seven Sketches in Compositionality: An Invitation to Applied Category Theory [fong-spivak-seven-sketches-2019]

January 1, 2019
Fong, Brendan, Spivak, David I.

Backlinks

Definition. Monotone function [0029]

November 25, 2025

A monotone function (or monotone map) between two preorders \((A, \leq _A)\) and \((B, \leq _B)\) is a function \(f: A \to B\) that preserves the order relation. This means that for all elements \(x, y \in A\), if \(x \leq _A y\), then it must also hold that \(f(x) \leq _B f(y)\). In other words, the function \(f\) does not reverse the order of elements when mapping them from set \(A\) to set \(B\). Formally:(1)

\[ \forall x, y \in A.\ x \leq _A y \implies f(x) \leq _B f(y) \]

Definition. Partial order [002d]

November 25, 2025

Remarks

November 25, 2025


    some piece of code

A partial order is just a preorder with an additional property called antisymmetry. A partial order on a set \(P\) is a binary relation \(\leq \) that satisfies the following three properties for all elements \(a, b, c \in P\):

\(a \leq a\) (Reflexivity): Every element is related to itself.
\(a \leq b \land b \leq c \to a \leq c\) (Transitivity): If an element \(a\) is related to \(b\), and \(b\) is related to \(c\), then \(a\) is also related to \(c\).
\(a \leq b \land b \leq a \to a = b\) (Antisymmetry): If an element \(a\) is related to \(b\), and \(b\) is related to \(a\), then \(a\) and \(b\) must be the same element.

More accurately a partial order is a reflexive, weak, non-strict partial order. Also known as skeletal preorder. [0]

Definition. Preorder relation [002a]

November 25, 2025

A preorder relation is a binary relation \(\preceq \) on a set \(S\) that is both reflexive and transitive. This means that for all elements \(a, b, c \in S\), the following conditions hold:(1)

\(x \preceq x\) (Reflexivity): Every element is related to itself.
\(a \preceq b \land b \preceq c \to a \preceq c\) (Transitivity): If an element \(a\) is related to \(b\), and \(b\) is related to \(c\), then \(a\) is also related to \(c\).

We denote the case of \(x\) and \(y\) being equivalent using the notation \(\equiv \) under the following conditions

\[ x \equiv y \iff x \preceq y \land y \preceq x \]