thin.cppm File Reference

Thin categories — categories whose hom-sets contain at most one morphism. More...

#include <concepts>
#include <functional>
import dedekind.category:mereology;

Include dependency graph for thin.cppm:

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsThinCategory
	A category in which every hom-set has at most one morphism.

Detailed Description

Thin categories — categories whose hom-sets contain at most one morphism.

@partition :thin

thin__Categorical_Definition

A thin (or posetal-shaped, in the textbook's looser usage) category is one in which hom(a, b) has at most one morphism for any pair of objects. Equivalently: any two parallel morphisms are equal.

In the order-theoretic encoding the codebase uses across :mereology and :posetal, this corresponds to a preorder over T with relation Rel and truth-value codomain L::Ω:

• Objects are elements of T.
• The unique morphism a → b (when it exists) is the witness of Rel(a, b) = L::True.
• Identity morphism id_a corresponds to reflexivity (Rel(a, a) = L::True).
• Composition corresponds to transitivity (Rel(a, b) ∧ Rel(b, c) ⇒ Rel(a, c)).

thin__Distinction_from_Posetal

IsThinCategory does not require antisymmetry. A thin category is a preorder, not necessarily a partial order; isomorphic objects need not be identical. Adding antisymmetry yields :posetal::IsPosetal — a thin category that is also skeletal.

IsPosetal is a strict refinement of IsThinCategory. At the time of this partition's introduction the inclusion is not yet encoded definitionally in IsPosetal — that signature-level refactor lands in #698 Slice 1, after which the inclusion is visible directly in IsPosetal's requires clause per the project's "faithful specialization in the type signature from day 1" posture.

thin__Sollbruchstelle_From_Small

:small's docstring deliberately defers thin-category vocabulary: "thin, discrete, locally-finite, intensional / extensional, lazy / strict — are also intentionally out of scope here; they are named (or named-able) at downstream partitions where they have semantic content." This partition closes that seam directly.

thin__Boolean_Witness

bool with std::less_equal participates: the 2-element poset (false ≤ true) is the smallest non-trivial thin category and a canonical entry point to the Form-chain (#698).

See also

https://en.wikipedia.org/wiki/Preorder

https://ncatlab.org/nlab/show/thin+category

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"Two parallel arrows in a thin category are equal --- the relation IS the morphism."