Operator symbols should match relations symbols (in lattices)

[andreasabel]

The usual convention in math is that the shapes of inf/sup-operators are chosen consistent with the shape of the comparison relation, with typical flavors being:

• rectangular
• round
• triangular

Thus the choice of a rectangular operator symbol in connection with a triangular relation symbol seems unnatural to me:

agda-stdlib/src/Algebra/Construct/NaturalChoice/Min.agda

Lines 29 to 37 in fb1d6f4

	_⊓_ : Op₂ A
	x ⊓ y with total x y
	... | inj₁ x≤y = x
	... | inj₂ y≤x = y
	------------------------------------------------------------------------
	-- Properties
	x≤y⇒x⊓y≈x : ∀ {x y} → x ≤ y → x ⊓ y ≈ x

Also, isn't the standard style for lattice operations the triangular one?

[MatthewDaggitt]

That seems like a reasonable convention. I took the square operators purely because they were the ones being used in Data.(Nat/Integer/Rational).Base....