Consequences as consequences for properties, or consequences for structured sets?

[HuStmpHrrr]

I find that there is a duplication between *.Consequences and *.Properties for structured sets, mainly including algebraic and order theories. I find the line between the consequences from functional properties and ones from structured sets is very blurred.

Consider, for example, https://github.com/agda/agda-stdlib/blame/master/src/Algebra/FunctionProperties/Consequences.agda#L103

assoc+id+invʳ⇒invˡ-unique : ∀ {_•_ _⁻¹ ε} →
                           Congruent₂ _•_ → Associative _•_ →
                           Identity ε _•_ → RightInverse ε _⁻¹ _•_ →
                           ∀ x y → (x • y) ≈ ε → x ≈ (y ⁻¹)

This law effectively unpacks monoid into a bunch of antecedents, plus a right inverse. Shouldn't it be something like

monoid+invʳ⇒invˡ-unique : ∀ {_•_ _⁻¹ ε} → IsMonoid _•_ ε → RightInverse ε _⁻¹ _•_ →
                           ∀ x y → (x • y) ≈ ε → x ≈ (y ⁻¹)

?

Then it's very clear by reading it as what if a monoid possesses some other things, what happens. I sometimes find claiming laws like this in *.Consequences is an overkill. Any thoughts on drawing a line?

[MatthewDaggitt]

So the problem is that you can't use IsMonoid in Algebra.FunctionProperties.Consequences as Algebra.Structures depends on it so you end up with a dependency cycle. You're right though that the above identity should probably be in Algebra.Properties.Monoid...

You're right though, it's difficult to draw the line. Hypothetically if the above property didn't require congruence, where would it belong then?

[JacquesCarette]

Not requiring congruence would be very weird... even a Magma requires it, no? Hmm, I notice Magma isn't even defined in Algebra.Structures!

[HuStmpHrrr]

i think congruence can be one of the criteria. The dilemma here is "what properties we want to put as a part of the definitions", which effectively prevents us from deriving properties from structured sets. if we view it in this way, it's a modularity problem in probably all languages.

Though, if a property is easy, what prevents us from inlining the definitions directly?

[JacquesCarette]

The drawback of inlining definitions is that this makes the recognition problem much harder: to 'see' that in two apparently dissimilar situations, there is actually a large core that is common, and can be abstracted out. By naming definitions that recur, the recognition problem becomes easier.

Which is, in fact, the core of your suggestion regarding using IsMonoid in this issue!

[HuStmpHrrr]

I guess there are different understandings of inlining here. I should probably pick another word. I think the recognition problem should only be about recognizing structures, instead of a set of properties. For example, in commutative monoid, deriving identityʳ uses left identity and commutativity.

https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L67

One rarely considers a set of properties in isolation. Monoid is already a very general and common structure. Suppose we directly prove right identity, I don't think we lose too much generality. A structure with no more information than left identity and commutativity is strange. Sure, if a larger proof requires right identity here, we should not inline the proof of left identity and commutativity there.

[JacquesCarette]

That proof really belongs in a 'left unital commutative semigroup'; and that would then make it provable that it is in fact a commutative monoid.

At this level, that sounds a bit ridiculous. But in other situations, when the proof is non-trivial, or higher up (semigroupoid), then these do start to matter.

[MatthewDaggitt]

Hmm, as I mentioned earlier in the thread, the Consequences files are often useful (/vital) to have when you don't necessarily have a full algebraic structure constructed yet. As this issue doesn't seem to have a concrete suggestion, and that I don't think the current situation is actively problematic, I'm going to close this for now.