dedekind::category::IsBoundedLatticeCategory Concept Reference

A lattice category that has a designated bottom (initial) and top (terminal) element — row 5 of the lattice Form-chain (#698 Slice 4). More...

Concept definition

template<typename T, typename Rel std::less_equal<T>, typename Join Sup, typename Meet Inf, typename L Boole>
concept dedekind::category::IsBoundedLatticeCategory = 
    IsLatticeCategory<T, Rel, Join, Meet, L> &&  
    IsInitialObject<LatticeBottom<T, Rel>> &&    
    IsTerminalObject<LatticeTop<T, Rel>> &&      
    requires {
      
      { LatticeBottom<T, Rel>::value } -> std::convertible_to<T>;
      { LatticeTop<T, Rel>::value } -> std::convertible_to<T>;
    }

Detailed Description

A lattice category that has a designated bottom (initial) and top (terminal) element — row 5 of the lattice Form-chain (#698 Slice 4).

Faithful inclusion IsBoundedLatticeCategory ⊊ IsLatticeCategory encoded definitionally per the project's "faithful specialization in the type signature from day one" posture (#698).

The bounded refinement adds two structural witness types:

• LatticeBottom<T, Rel> — declared as an initial-object witness via :limit::IsInitialObject (relaxed with tag-discovery).
• LatticeTop<T, Rel> — declared as a terminal-object witness via :limit::IsTerminalObject (relaxed similarly).

These are the lattice's own initial / terminal objects — universal-property witnesses local to the lattice over (T, Rel) viewed as a thin category. Distinct from the strict-global std::same_as<T, Zero> / std::same_as<T, One> branches of the :limit concepts, which name the unique initial / terminal of the ambient category of sets. The tag-discovery relaxation of :limit (in turn) admits both readings without parallel concept surface.

Faithful per #698 Q3: the Form-chain commits to categorical universal-property witnesses — bottom / top are designated structural witness types satisfying IsInitialObject / IsTerminalObject, not operational lower_bound() / upper_bound() member functions on a Sub.

Template Parameters

T	The Domain (Objects).
Rel	The Relation.
Join	The join operation (default Sup).
Meet	The meet operation (default Inf).
L	The Logic Species.