A bounded lattice category whose lattice exponentials are witnessed by :cartesian::IsExponential — row 6 of the lattice Form-chain (#698 Slice 6). More...

Concept definition

template<typename T, typename Rel std::less_equal<T>, typename Join Sup, typename Meet Inf, typename L Boole>
concept dedekind::category::IsHeytingLatticeCategory = 
    IsBoundedLatticeCategory<T, Rel, Join, Meet,
                             L> &&  
    IsExponential<HeytingExponential<T, Rel, Meet>, T,
                  T>

Detailed Description

A bounded lattice category whose lattice exponentials are witnessed by :cartesian::IsExponential — row 6 of the lattice Form-chain (#698 Slice 6).

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

lattice__Heyting_Form_Chain_Row_6

The Heyting refinement requires the carrier T has an exponential object structure: HeytingExponential<T, Rel> wraps the relative complement value a → b and satisfies :cartesian::IsExponential. The structural alignment with the CCC concept means lattice exponentials and function-space exponentials inhabit the same categorical surface — different concrete representations, one shared concept (#698 Slice 6's generalisation of IsExponential).

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.