equivalence.cppm File Reference

Equivalence relations: reflexive + symmetric + transitive predicates, composing the existing axiom traits in :species with a new symmetry trait. More...

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

Include dependency graph for equivalence.cppm:

Classes
struct	dedekind::category::is_symmetric< T, Rel >
	Engineer-supplied trait: relation Rel on T is symmetric (∀x, y: Rel(x, y) ⇔ Rel(y, x)). More...
struct	dedekind::category::is_symmetric< T, Rel >
struct	dedekind::category::is_equality< T, Rel >
	Trait: Rel on T is equality, the diagonal Δ: Rel(a, b) holds iff a and b are the same value. More...
struct	dedekind::category::is_equality< T, Rel >
struct	dedekind::category::is_equality< T, std::equal_to< T > >
struct	dedekind::category::is_equality< T, std::equal_to<> >
struct	dedekind::category::is_equality< std::pair< A, B >, std::equal_to< std::pair< A, B > > >
struct	dedekind::category::is_equality< std::pair< A, B >, std::equal_to<> >
struct	dedekind::category::is_reflexive< T, Rel >
struct	dedekind::category::is_transitive< T, Rel >
struct	dedekind::category::is_antisymmetric< T, Rel >
struct	dedekind::category::detail_equality::SameInt
	A carrier's own equality, certified once: the laws follow. More...
struct	dedekind::category::is_equality< int, detail_equality::SameInt >
struct	dedekind::category::is_equality< detail_mereology::Dial< 3 >, std::equal_to< detail_mereology::Dial< 3 > > >

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsSymmetric
	Formal verification: Rel(a, b) ⇔ Rel(b, a).
concept	dedekind::category::IsEquality
	Rel on T is equality of values (the diagonal).
concept	dedekind::category::IsChainDecidedSymmetric
	Symmetry, stated once for every relation on a walkable chain.
concept	dedekind::category::IsEquivalence
	A binary relation on T that is reflexive, symmetric, and transitive — the textbook equivalence-relation axioms.
concept	dedekind::category::IsHashFunction
	A callable h on T whose codomain is std::size_t — i.e. an arrow T → size_t.

Functions
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::symmetric_at (const Rel &rel, const T &a, const T &b)
	Symmetry at a point (mereology__The_Laws_At_A_Point).
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::symmetric_on (const Rel &rel, const T &lo, const T &hi)
	Symmetry over a whole chain (mereology__The_Laws_On_A_Chain).
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { x == x } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::equality_at (const Rel &rel, const T &a, const T &b)
	Equality at a point: the relation answers as == does.

Variables
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_symmetric_v = is_symmetric<T, Rel>::value
	The "v" helper following the :species convention.
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_equality_v = is_equality<T, Rel>::value

Detailed Description

Equivalence relations: reflexive + symmetric + transitive predicates, composing the existing axiom traits in :species with a new symmetry trait.

@partition :equivalence

Copyright

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

equivalence__Motivation

The textbook equivalence relation R on a carrier T is reflexive (R(x, x)), symmetric (R(x, y) ⇔ R(y, x)), and transitive (R(x, y) ∧ R(y, z) ⇒ R(x, z)). These three properties are universal-property territory: the type system can name the predicate shape (a binary relation on T returning a logical value), but cannot quantify over all x, y, z to verify the axioms. Per the project's honesty obligation pattern, each axiom is an engineer-supplied trait specialisation; the compiler trusts the declaration; the public review process is the audit trail.

Reflexivity and transitivity already live in :species (is_reflexive_v<T, Rel> and is_transitive_v<T, Rel>, with the canonical specialisations on std::less_equal that the partial-order machinery in :posetal builds on). This partition adds the missing symmetry trait and bundles all three into a single IsEquivalence<T, Rel> concept.

equivalence__The_Mazur_Reading

Per Barry Mazur's When is one thing equal to some other thing? (in Gold & Simons (eds.), Proof and Other Dilemmas, MAA 2008), an equivalence relation is the principled way to relax strict equality without abandoning the algebraic gate: a carrier T can be treated as inhabiting a stricter algebraic concept when the laws hold up to a named equivalence relation, even if they don't hold under == in the bit-perfect sense. This partition lays the structural foundation for that escape hatch (filed under #591); the first concrete pilot is std::unsigned_integral as ℕ for ``sufficiently small'' inputs, wired in numbers:uint.

equivalence__Use_cases

• Bounded equivalence: uint64_t under modular arithmetic equates to ℕ for inputs strictly less than 2^64; the equivalence captures the ``sufficiently small'' qualification at the type level. Pilot in numbers:uint.
• ε-equivalence on IEEE doubles: |a - b| < eps; lifts double's non-strict-field arithmetic into the algebraic gate. Future work; depends on the unsigned pilot landing first.
• Quotient algebras: A/~ as a carrier requires the equivalence relation ~ on A that defines the quotient (sister motivation to IsQuotientAlgebra in algebra:quotient).

See also

Mazur, B. (2008), When is one thing equal to some other thing?, in Gold & Simons (eds.), Proof and Other Dilemmas: Mathematics and Philosophy, MAA, pp. 221–242.

Note

"No entity without identity." — Willard Van Orman Quine, Theories and Things (Harvard University Press, 1981), Ch. "Things and Their Place in Theories".