Split out ComplementedLattice from Heyting typeclass?

(Ok I'm being slightly tongue in cheek, but..) IMO it's an unfortunate accident of history that the lattice algebra hierarchy ended up in a ecosystem-anchor library like Cats.

On one hand, it begs to become the butt of jokes. A workmate used to ask if anyone had "designed any lattices lately?".

OTOH it means that evolving the lattice typeclasses becomes a more heavyweight change than in Spire or another more obscure location.

The Heyting typeclass introduced two new, independent abstract methods, complement and imp (implication).

https://github.com/typelevel/cats/blob/main/algebra-core/src/main/scala/algebra/lattice/Heyting.scala#L64-L65

Introducing two distinct abstract operations in a single TC may be a design smell. Is there a weaker form with just one?

Yes, an algebra that has just complement without imp is called a Complemented Lattice.

Why does it matter? Well, a datatype for proper fraction, a value between [0, 1], could implement ComplementedLattice and complement is useful. But I can't see a sensible implementation for imp that would get used; that operator seems to belong in discrete logics.

Start with algebra-core/src/main/scala/algebra/lattice/Heyting.scala and inspect the existing complement and imp methods in the Heyting typeclass. Compare the proposed ComplementedLattice abstraction with the linked lattice hierarchy and determine whether the API should separate the operations; done means reaching and documenting a settled design decision.