Posetal categories — categories derived from partial orders. More...

#include <algorithm>
#include <array>
#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
#include <variant>
import dedekind.category:thin;

Include dependency graph for posetal.cppm:

Classes
struct	dedekind::category::monotone_trait< F, Op >
	User-declared monotonicity witness for an arrow type `F` with respect to the ambient order relation `Op`. More...
struct	dedekind::category::antimonotone_trait< F, Op >
	User-declared anti-monotonicity witness for an arrow type `F` with respect to the ambient order relation `Op`. More...
struct	dedekind::category::Profile< E, N >
	The laws an arrow is known to have, one answer in K₃ per law: `True` where certified, `Unknown` where not, never `False` (a profile certifies, it does not refute). The pointwise lift Ω^E of the truth chain to the laws (`lattice__Omega_First_Pointwise_Lift`), restricted to its sub-chain Σ = {Unknown < True}: combined law by law with `Inf` / `Sup`. Read by the laws of functions below and by the laws of relations (`relational:dyadic`). More...
struct	dedekind::category::ArrowNodeAt
	The engine at one former and one law, as a function of the law. More...
struct	dedekind::category::ProductLeq< LeqA, LeqB >
	Componentwise product order on `std::pair` `≤×:` (a,c)≤(b,d) :⟺ `a≤b` `∧` `c≤d`. The order-theoretic product of two posets, not the lexicographic `std::less_equal` on the pair. More...
struct	dedekind::category::detail_ordinal_sum::Unordered

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsPosetal
	A Category where morphisms are governed by a specific Logic Species (Ω).
concept	dedekind::category::IsTotallyOrderedPosetal
	Posetal refinement where the underlying order is total/linear.
concept	dedekind::category::IsOrderMeetSemilattice
	Order-theoretic meet-semilattice as a commutative refinement.
concept	dedekind::category::IsCertifiedOrderMeetSemilattice
	Trait-certified meet-semilattice (associative + idempotent + commutative).
concept	dedekind::category::IsOrderJoinSemilattice
	Order-theoretic join-semilattice as a commutative refinement.
concept	dedekind::category::IsCertifiedOrderJoinSemilattice
	Trait-certified join-semilattice (associative + idempotent + commutative).
concept	dedekind::category::IsOrderLatticeOperations
	Order-theoretic lattice operations as commutative + absorptive refinement over upstream mereological lattice operations.
concept	dedekind::category::IsCertifiedOrderLatticeOperations
	Trait-certified lattice operations (commutative semilattices + absorption).
concept	dedekind::category::IsOrderDistributiveLatticeOperations
	Distributive lattice refinement over IsOrderLatticeOperations.
concept	dedekind::category::IsCertifiedOrderDistributiveLatticeOperations
	Trait-certified distributive lattice refinement.
concept	dedekind::category::IsPathProjection
	Projection contract used by check_path to map objects into an orderable relation carrier.
concept	dedekind::category::IsMonotone
	An arrow `F` declared to be order-preserving with respect to the ambient order relation `Op`.
concept	dedekind::category::IsAntiMonotone
	An arrow `F` declared to be order-reversing with respect to the ambient order relation `Op`.
concept	dedekind::category::IsVariant
	An arrow with a definite variance: order-preserving (`IsMonotone`) or order-reversing (`IsAntiMonotone`). The leg-shape of a Galois connection, whose adjoints are always one or the other. Mirrors :limit::IsBoundaryObject's `"X @c \|\| @c dual"` disjunction shape.
concept	dedekind::category::IsOrderIsomorphism
	An arrow that is both an order-preserving map and a bijection.
concept	dedekind::category::IsOrderAntiIsomorphism
	An arrow that is both an order-reversing map and a bijection.
concept	dedekind::category::HasDomain
	A type that names its domain: `Dom<F>` is formed. The guard under which `IsInvolution<F>` may be asked at all.

Typedefs
using	dedekind::category::DefaultJoin = Sup
using	dedekind::category::DefaultMeet = Inf
using	dedekind::category::ArrowLaws = Profile<ArrowLaw, every_arrow_law.size()>
	The profile of a function.

Enumerations
enum class	dedekind::category::ArrowLaw : unsigned { Injective , Surjective , Monotone , Antitone , Involutive , Constant }
enum class	dedekind::category::ArrowNode { Compose , Product , Sum , Pairing , Copairing }
	The formers of arrows: g ∘ f, f × g, f + g, ⟨f, g⟩, [f, g].

Functions
template<typename T, typename Rel = std::less_equal<T>, typename L = Boole, typename Project = std::identity> requires IsPathProjection<Project, T, Rel, typename L::Ω>
constexpr L::Ω	dedekind::category::check_path (T a, T b, T c, Project project={})
	Verify that a two-step path A→B→C exists in the posetal category.
template<typename Whole> requires requires { arrow_drill_down(whole).min; }
constexpr auto	dedekind::category::arrow_drill_down_min (const Whole &whole)
	Opt-in drill-down projector for min/max result carriers.
constexpr Ternary	dedekind::category::monotone (ArrowLaws p)
	What a profile says about monotonicity: the law read off the fold's result, in K₃ (`True` where certified, `Unknown` where not).
constexpr Ternary	dedekind::category::infer (ArrowLaw w, ArrowNode n, const ArrowLaws &a, const ArrowLaws &b)
	The engine at one law: a former's answer from its legs' profiles, their laws combined by the chain's own `Inf` (both legs) and `Sup` (either leg). The facts, each a theorem about functions:
constexpr ArrowLaws	dedekind::category::saturated (ArrowLaws p)
	Entailment, a closure operator on profiles: an involution is its own inverse, so a bijection. Nothing is entailed about a constant arrow's variance here: it is monotone and antitone under a reflexive order and neither under a strict one, and a profile is read under an arbitrary order; the typed reader has the fact where the order is in reach (:total). Nor the converse, monotone and antitone entailing constant, which holds on a connected domain only. The engine applies the entailment to values; a typed arrow already has it through the iso hook (:involution).
constexpr ArrowLaws	dedekind::category::without_variance (ArrowLaws p)
	The laws that do not depend on an order: a profile read under an order the former's variance facts are not about.
constexpr ArrowLaws	dedekind::category::arrow_node (ArrowNode n, const ArrowLaws &a, const ArrowLaws &b)
	The engine at a former, law by law, its legs and its answer saturated.
template<typename F, typename Op>
constexpr ArrowLaws	dedekind::category::declared_arrow_laws ()
	The profile of a typed arrow, its variances under `Op`. Read off the concepts (an iso, hence an involution, is already monic and epic).
template<IsArrow F>
constexpr bool	dedekind::category::is_identity (const F &)
	The laws of an arrow asked on its value (the Jlt paper's Listing 1): each reads, at compile time, the registration its concept reads, so `is_monic(f)` is `IsMonicArrow<F>` at the value's type, and a composite's law comes through the readers above. A concept gates a template, a predicate states a fact; both read one registration.
template<IsArrow F>
constexpr bool	dedekind::category::is_constant (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_monic (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_epic (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_iso (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_involution (const F &)
template<IsArrow F, IsArrow G> requires commutes_v<F, G>
constexpr bool	dedekind::category::is_involution (const Compose< F, G > &c)
	A composite of two commuting involutions is one, \((g f)^2 = g g f f = \mathrm{id}\), its law derived from its legs' (`commutes`, :involution); where the legs do not commute, the reading above decides, and `-` after `~` is none.
template<IsArrow F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_monotone (const F &, Op={})
template<IsArrow F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_antitone (const F &, Op={})
template<IsArrow F> requires std::unsigned_integral<Cod<F>> && (!std::same_as<Cod<F>, bool>)
constexpr auto	dedekind::category::operator~ (const F &f)
	The involutions of a codomain, pointwise on the arrows into it: `~f` and `-f` are `f` then the reflection of the chain, respectively unary minus, (-f)(x) `=` `-f(x)` as for functions in analysis; on an identity the composite is the involution itself (the unit law, :morphism). `!f`, for the arrows into a truth object, is in :topoi. Unsigned only: `-INT_MIN` is not a function on `int` (:involution); and not `bool`, which C++ counts as unsigned, so a set's characteristic arrow keeps the complement of :sets.
template<IsArrow F> requires std::unsigned_integral<Cod<F>> && (!std::same_as<Cod<F>, bool>)
constexpr auto	dedekind::category::operator- (const F &f)

Variables
constexpr std::ranges::min_max_result< int >	dedekind::category::p1 {1, 0}
constexpr std::ranges::min_max_result< int >	dedekind::category::p2 {2, 0}
constexpr std::ranges::min_max_result< int >	dedekind::category::p3 {3, 0}
template<typename F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_monotone_v
template<typename F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_antimonotone_v
template<typename T, typename Op>
constexpr bool	dedekind::category::is_monotone_v< Identity< T >, Op > = true
template<typename L, typename Op>
constexpr bool	dedekind::category::is_antimonotone_v< NegationArrow< L >, Op > = true
template<typename L, typename Op>
constexpr bool	dedekind::category::is_monotone_v< LiftLogic< L >, Op > = true
constexpr std::array< ArrowLaw, 6 >	dedekind::category::every_arrow_law
template<typename F, typename Op = std::less_equal<>>
constexpr ArrowLaws	dedekind::category::arrow_laws_v = declared_arrow_laws<F, Op>()
template<IsArrow F, IsArrow G>
constexpr bool	dedekind::category::is_monic_arrow_v< Compose< F, G > >
template<IsArrow F, IsArrow G>
constexpr bool	dedekind::category::is_epic_arrow_v< Compose< F, G > >
template<typename F, typename G, typename Op>
constexpr bool	dedekind::category::is_monotone_v< Compose< F, G >, Op >
template<typename F, typename G, typename Op>
constexpr bool	dedekind::category::is_antimonotone_v< Compose< F, G >, Op >
template<IsArrow F, IsArrow G>
constexpr bool	dedekind::category::is_constant_arrow_v< Compose< F, G > >
constexpr auto	dedekind::category::detail_posetal_value_laws::id_u = Identity<std::size_t>{}
template<typename A, typename B, typename LeqA, typename LeqB>
constexpr bool	dedekind::category::is_reflexive_v< std::pair< A, B >, ProductLeq< LeqA, LeqB > >
template<typename A, typename B, typename LeqA, typename LeqB>
constexpr bool	dedekind::category::is_transitive_v< std::pair< A, B >, ProductLeq< LeqA, LeqB > >
template<typename A, typename B, typename LeqA, typename LeqB>
constexpr bool	dedekind::category::is_antisymmetric_v< std::pair< A, B >, ProductLeq< LeqA, LeqB > >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_reflexive_v< std::variant< X, Y >, std::less_equal<> >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_transitive_v< std::variant< X, Y >, std::less_equal<> >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_antisymmetric_v< std::variant< X, Y >, std::less_equal<> >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_reflexive_v< std::variant< X, Y >, std::less_equal< std::variant< X, Y > > >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_transitive_v< std::variant< X, Y >, std::less_equal< std::variant< X, Y > > >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_antisymmetric_v< std::variant< X, Y >, std::less_equal< std::variant< X, Y > > >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_connex_v< std::variant< X, Y >, std::less_equal<> >
template<typename X, typename Y>
constexpr bool	dedekind::category::is_connex_v< std::variant< X, Y >, std::less_equal< std::variant< X, Y > > >

Detailed Description

Posetal categories — categories derived from partial orders.

@partition :posetal

posetal__Categorical_Definition

A Posetal Category is a category where for any two objects A and B, there is at most one morphism from A to B. In this framework:

Objects are elements of the set.
Morphisms represent the relation (a ≤ b).
Identity morphisms correspond to Reflexivity (a ≤ a).
Composition corresponds to Transitivity (a ≤ b and b ≤ c implies a ≤ c).
Skeletality in the category corresponds to Antisymmetry (a ≤ b and b ≤ a implies a = b).

posetal__Order_Structure

This structure corresponds to a Partially Ordered Set (Poset). Unlike a Preorder, a Posetal Category is skeletal, meaning isomorphic objects are identical.

Textbook defaults in this partition:

Relation defaults to std::less_equal<T> (the canonical order witness).
Logic defaults to Boole (Boolean Ω).

@quote "In a sense, the most basic category is a partially ordered set; the arrows are just the instances of the order relation." — Saunders Mac Lane, Categories for the Working Mathematician

See also: https://en.wikipedia.org/wiki/Partially_ordered_set; https://en.wikipedia.org/wiki/Preorder

Template Parameters

T	The type of objects in the poset.
Rel	The relation defining the order (the Morphism Generator).

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

Note: "Science, in other words, is a system of relations." – Henri Poincare, The Value of Science (1905)

Classes

Namespaces

Concepts

Typedefs

Enumerations

Functions

Variables

Detailed Description

posetal__Categorical_Definition

posetal__Order_Structure