The inclusion (subset) order on subobject lattices, derived from the structural meet and equality (#831). More...
#include <concepts>#include <type_traits>import dedekind.order:halfspace;import dedekind.category;
Concepts | |
| concept | dedekind::order::SubobjectLatticePair |
A compatible pair of subobject lattices — same ambient Domain and logic_species: the canonical rung on which subset is defined. Ties the order to category::IsSubobjectLattice rather than a bespoke shape; the same-logic clause is the cross-logic-mereology guard (#833 review). | |
| concept | dedekind::order::DecidableMeetSubset |
\(A \subseteq B\) is decidable via the structural meet: a subobject-lattice pair whose meet-then-equality is a truth value. The gate for the generic identity <=; where the meet does not collapse this is unsatisfied (the honest exists / forall wall) and a per-carrier <= must supply the case. | |
| concept | dedekind::order::HasSubset |
A decidable <= exists for the pair — generic (meet) or a per-carrier specialisation (Singleton membership, Interval endpoints). The gate for the derived relations, so they ride any <=, not only the meet-based one. | |
| concept | dedekind::order::HasProperSubset |
HasSubset plus a bool ==, so \(A \subsetneq B \equiv A
\subseteq B \wedge A \neq B\) is expressible. | |
Functions | |
|
template<typename A, typename B> requires DecidableMeetSubset<A, B> | |
| constexpr A::logic_species::Ω | dedekind::order::operator<= (const A &a, const B &b) |
\(A \subseteq B \iff A \cap B = A\) — the generic identity. More-specialized per-carrier <= (Set / Ø / 𝔸, the Singleton membership and Interval endpoints below) win by partial ordering; this fills the gaps (Halfspace ⊆ Halfspace). | |
|
template<typename A, typename B> requires HasSubset<B, A> | |
| constexpr A::logic_species::Ω | dedekind::order::operator>= (const A &a, const B &b) |
Superset, proper subset, proper superset — each once from <= and ==, gated on HasSubset so they ride any decidable <= (generic or specialised). Together they supply HasPartialOrderOperators. | |
|
template<typename A, typename B> requires HasProperSubset<A, B> | |
| constexpr A::logic_species::Ω | dedekind::order::operator< (const A &a, const B &b) |
|
template<typename A, typename B> requires HasProperSubset<B, A> | |
| constexpr A::logic_species::Ω | dedekind::order::operator> (const A &a, const B &b) |
| template<typename T, typename L> | |
| constexpr L::Ω | dedekind::order::operator<= (const Interval< T, L > &a, const Interval< T, L > &b) |
| \(A \subseteq B\) on intervals: \(A \cap B = A\), extensional since interval equality closes strict bounds on a discrete carrier. | |
Detailed Description
The inclusion (subset) order on subobject lattices, derived from the structural meet and equality (#831).
@partition :inclusion
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
Subset is the lattice identity \(A \subseteq B \iff A \cap B = A\) (Birkhoff §1.4), gated on the canonical rung category::IsSubobjectLattice; the strict / dual relations derive from <= and ==. Together they supply the surface HasPartialOrderOperators names.
It computes via the structural & operator, not the CT-vocabulary meet: the two diverge for structured carriers (#834) — & rides structured_and and collapses ({x>5} ∩ {x>3} = {x>5}), so only & makes the subset decidable. Per the operating model, the identity is the default and each concrete carrier proves its own decidability by a specialised <= (Ø / 𝔸 trivial, Singleton membership, non-empty Halfspace by pivot); those win by partial ordering, and this generic fills the gaps.
