Problems with change of `Semilattice` operation name

[MatthewDaggitt]

First issue with RC 1. Changelog doesn't mention that the name of the operation in Semilattice changed from _∧_ to _∙_.

More problematically the names in IsSemilattice have not been changed 😢

agda-stdlib/src/Algebra/Lattice/Structures.agda

Line 39 in a7d2302

open IsBand isBand public

[Taneb]

I'd like to address this more aggressively, by tying it with #2138 and removing the undirected IsLattice etc structures entirely.

[jamesmckinna]

Don't remove: deprecate!

[jamesmckinna]

@Taneb Any progress on this issue/PR?

[jamesmckinna]

Cf. #2178 what is the operator symbol supposed to be in Semilattice?
I'm starting to wonder/panic whether that PR actually did the right thing?

[MatthewDaggitt]

Should be the dot symbol. In the interests of getting the next RC out the door I'm taking this one over.

[Taneb]

Sorry, I've been sick lately. I'm only just getting enough brainpower back to write Agda now