Algebraic semilattice theories are missing

[HuStmpHrrr]

What do you think?

In Algebra, only Lattice is defined. However, Semilattices are going to be helpful. I can do it in May if it's wanted.

#439 might also need to be considered if we want to complicate various order theoretic definitions.

[MatthewDaggitt]

I think it already exists. The algebras are classified by the number and types of operators so it's near the top of the file with semigroups.

agda-stdlib/src/Algebra.agda

Lines 78 to 85 in e9c6f57

	record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
	infixr 7 _∧_
	infix 4 _≈_
	field
	Carrier : Set c
	_≈_ : Rel Carrier ℓ
	_∧_ : Op₂ Carrier
	isSemilattice : IsSemilattice _≈_ _∧_

[HuStmpHrrr]

yeah that's true. what about bounded semilattice? that one I believe is missing. I am looking for the same concepts in algebras that have been implemented on the order theoretical side. I believe both bounded semilattice and bounded lattice are missing. I need to reason these algebraic structures recently, hence the question.

[MatthewDaggitt]

Yup, there's no bounded semilattice so feel free to add it. The next question is what structure it inherits from...

The idea that I've been using so far is group the hierarchy by the signature of its operators. This is the only way I can see of doing it consistently, as the names of such structures aren't particularly consistent.
Therefore in this case BoundedSemilattice should inherit from CommutativeMonoid rather than Semilattice.

[JacquesCarette]

I've got a couple hundred theories that should be considered if we're going to start down that road.

Also, the above IsSemilattice is on two arguments but

agda-stdlib/src/Algebra/Structures.agda

Lines 54 to 57 in e9c6f57

	record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
	field
	isBand : IsBand ∧
	comm : Commutative ∧

has only one. [I used the experimental branch, is that right?]. So something's odd there.

[MatthewDaggitt]

@HuStmpHrrr just found bounded semilattices, they're called IsIdempotentCommutativeMonoid in the file.

Also, the above IsSemilattice is on two arguments but ... has only one. So something's odd there.

@JacquesCarette If I understand your question correctly, the equality is missing because it's provided as a module parameter at the top of the file.

[HuStmpHrrr]

@MatthewDaggitt wow indeed, it's so hard to notice. what about creating an alias for it?

[JacquesCarette]

That is indeed not an obvious place to look for IsEquivalence. But I guess it makes sense, now that I think about it.

Note that having an 'alias' IsBoundedLattice for IsIdempotentCommutativeMonoid would massively improve findability! You're expecting your readers to know too much Algebra.

[MatthewDaggitt]

@MatthewDaggitt wow indeed, it's so hard to notice. what about creating an alias for it?

Yup! Sounds like a plan! Note that you'll also need to create an alias for the module as well so that people can write open IsBoundedSemilattice.

[MatthewDaggitt]

Note that having an 'alias' IsBoundedLattice for IsIdempotentCommutativeMonoid would massively improve findability! You're expecting your readers to know too much Algebra.

Haha no expectations on my part! I only myself realised that the two were equivalent when I read up on them just now.

[laMudri]

So, I notice we have a few lattice-like structures in Algebra, and a more comprehensive collection in Relation.Binary.Lattice. Also, this new definition of BoundedLattice in Algebra is incorrect as far as I understand; it should be BoundedSemilattice. It's also not by necessity that this one can't have lattice-like notation; open ... public renaming (...) should be used here.

I think it would be nice to deprecate all of the lattice stuff in Algebra in favour of the structures in Relation.Binary.Lattice, and then have lemmas somewhere relating idempotent commutative structures to lattices.

[HuStmpHrrr]

you are very much correct. it should be BoundedSemilattice. what I don't follow is the second part: the two groups of definitions of lattices are not the same. why would you remove the algebraic definitions?

[JacquesCarette]

It can be very useful (even in Univalent settings) to have 2 equivalent formulations of a complex theory. Bill Farmer, Michael Kohlhase and I have dubbed such settings 'realms'. The point is that in practice, one 'interface' to a theory (like Lattice) might be much easier to work with than the other. Forcing computations to necessarily translation can be very inefficient. In other words, I am very happy with the redundancy of definition of theories.

[laMudri]

I was thinking the difference between the two definitions wasn't really that much, but maybe starting from the order versus starting from the operator(s) is big enough to warrant having the two separately. In that case, the collection of definitions in Algebra probably should be improved.

More generally, I agree that equivalent formulations are just as important in univalent and non-univalent settings.

[MatthewDaggitt]

Bounded semilattices are being added in #1108