\(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. More...

Concept definition

template<typename A, typename B>
concept dedekind::order::DecidableMeetSubset = 
    SubobjectLatticePair<A, B> && requires(const A& a, const B& b) {
      { (a & b) == a } -> std::convertible_to<typename A::logic_species::Ω>;
    }

Detailed Description

\(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.