Add derived (pre-)groupoid operations to Relation.Binary.Is(Partial)Equivalence

[jamesmckinna]

This is a partial resolution of the second part of #2247 .

Currently, the design (wrt notation/naming, infix, exports, etc.) is speculative and up for discussion, ahead of considering propagating the use of the new combinators to the many places in the library where they might be used for more streamlined equational reasoning:

• Algebra.Construct.LexProduct.Inner (4 occurrences)
• Algebra.Construct.NaturalChoice.MinOp (5 occurrences)
• Algebra.Properties.CommutativeSemigroup (11 occurrences)
• Algebra.Properties.Semiring.Divisibility (2 occurrences)
• Axiom.UniquenessOfIdentityProofs (4 occurrences)
• Codata.Guarded.Stream.Relation.Binary.Pointwise (8 occurrences)
• Data.Container.Relation.Unary.Any.Properties (2 occurrences)
• Data.Integer.Properties (12 occurrences)
• Data.List.Countdown (7 occurrences)
• Data.List.Fresh.Membership.Setoid.Properties (2 occurrences)
• Data.List.Membership.Propositional.Properties (2 occurrences)
• Data.List.Membership.Setoid.Properties.agda (4 occurrences)
• Data.List.Relation.Binary.BagAndSetEquality (3 occurrences)
• Data.List.Relation.Binary.Permutation.Propositional.Properties (5 occurrences)
• Data.List.Relation.Binary.Permutation.Setoid.Properties (12 occurrences)
• Data.List.Relation.Unary.Unique.Setoid.Properties (2 occurrences)
• Data.Vec.Recursive.agda (2 occurrences)
• Data.Vec.Relation.Binary.Equality.Cast (3 occurrences)
• Data.Vec.Relation.Unary.Any.Properties (2 occurrences)
• Relation.Binary.Construct.Closure.SymmetricTransitive (3 occurrences)
• Relation.Binary.Properties.Setoid (2 occurrences)
• Relation.Binary.PropositionalEquality (8 occurrences)
• Relation.Binary.PropositionalEquality.Properties (2 occurrences)

plus a further 20+ modules with a single occurrence of one of the combinations.

UPDATED: I'm conscious of the discussion elsewhere of the Fairbairn threshhold, and wondering if this proposal meets it?

[MatthewDaggitt]

UPDATED: I'm conscious of the discussion #669 (comment) of the Fairbairn threshhold, and wondering if this proposal meets it?

Again, my personal view is that it doesn't....

I'm also not that keen on the name for two reasons. Firstly it is not consistent with the naming style for other combinators in the Setoid hierarchy. Secondly, it's kind of a common name, so I'm kind of reluctant to pollute every namespace that ever opens a Setoid with it. I suspect this would break a lot of user code.... (it certainly breaks some of my personal library)

[jamesmckinna]

Thanks Matthew for the feedback!

On syntax per se, I agree that the proposed additions differ/diverge from existing stdlib convention but that's partly, again in my opinion, that the library isn't that good at supporting infix proof combinators, for whatever reason. But the particular trans ... (sym ...) pattern seems sufficiently common (witness the task list above) to merit the addition, although without agreeing in principle to the idea, I wasn't about to systematically apply it throughout...

On the actual choices of name, which name(s) clash for you, or all of them? I can/could/might see that _⊗_ might be a deal-breaker, but that's the one I'd find easiest to jettison, other than it's being the 'root' syntax for the others...

[JacquesCarette]

Hate the name too.

However, I've defined (and used) a combinator for this a lot in agda-categories. See the bottom of Category.Core for the details.

While it completely fails the threshold, the increase in readability of some code very strongly makes up for it.

Personally, I'd rather use some kind of 'fat semi colon' instead of a variant on a composition operator. And my 'flip' operation is too big.

[jamesmckinna]

OK, @JacquesCarette so "hate" is strong, but perhaps grabbing _⊗_ is too much of a 'provocation', except that from my perspective, transitivity (and its name) do derive from the underlying bicategory/groupoid structure of relational/equational proofs, so it seemed 'ok' to deploy the symbol here... but I'm happy for the pushback.

I'll look at your usage in agda-categories... and think some more. I'm personally happy to stick to the new prefix names, if they were accepted, and only the infix symbolic names for those. But it seems as though this might need more discussion!

(I'm not personally a fan, in my own turn, for semicolon-based symbology, especially the 'fat' one, so it's unfortunate that taste seems so caught up in library design issues; a case of Wadler's laws perhaps?)

[JacquesCarette]

There are times where strong language is the simplest way to communicate one's strong feelings, especially in a written medium like this. I wanted no ambiguity.

I think I see things differently here: transitivity does not derive from the structure of equational proof, but is part of the defining structure of being an "equational proof structure", i.e. structure vs property. You prove that things satisfy the API of being a groupoid, you don't start with an arbitrary groupoid.

I'm fine with picking something other than a semicolon; I do think that since trans is fundamentally ordered, we should not pick a symmetric symbol for it. So agda-categories's choice there is downright bad too!

[MatthewDaggitt]

I'm still not super keen on this idea, but if you are keen to push for it @jamesmckinna then my naming suggestions would be trans-symˡ and trans-symʳ

[MatthewDaggitt]

Ah drat, that name is already taken the proof about it... https://github.com/search?q=repo%3Aagda%2Fagda-stdlib%20trans-sym%CB%A1&type=code

[JacquesCarette]

On revisit, I think I'm siding with @MatthewDaggitt on this (i.e. not keen). If one were to use equational reasoning in these cases, all the needed kit is already in place. So this only saves a little bit when doing equational proofs inline.

I think it's actually a good idea to not make those 'convenient' !

[jamesmckinna]

I take the consensus view: the 'Noes' have it!