The CODOMAIN Ω of a leaf / term, dual to carrier_of (the domain). A predicate / subobject leaf is an arrow χ:Domain→Ω, so its codomain is Ω (the subobject classifier), read via ::Codomain. A bare value leaf is a truth value, so its codomain is its own type (domain = codomain there, which is why the two-element bool lattice behaves identically under either accessor). Composites propagate the common Ω (fail-closed, exactly like carrier_of). More...

Public Types
using	type = void

Detailed Description

template<typename X>
struct dedekind::category::codomain_of< X >

The CODOMAIN Ω of a leaf / term, dual to carrier_of (the domain). A predicate / subobject leaf is an arrow χ:Domain→Ω, so its codomain is Ω (the subobject classifier), read via ::Codomain. A bare value leaf is a truth value, so its codomain is its own type (domain = codomain there, which is why the two-element bool lattice behaves identically under either accessor). Composites propagate the common Ω (fail-closed, exactly like carrier_of).

Complementation and De Morgan negation are properties of the CODOMAIN lattice Ω, not the domain: Sub(X) is complemented iff Ω is (Boole yes; Kleene's 3-chain no, ¬U=U). So the complement / De Morgan laws gate on codomain_of (this), while SameCarrier and the glb collapse — "are these over the same ambient?" — stay on carrier_of (the domain). This is the domain/codomain disentanglement: the reducer stays vanilla (semi-)lattice and simply asks "is @c Ω complemented?".

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/lattice.cppm

Public Types

Detailed Description