A more declarative auto-cong machinery

[gallais]

I have written a little bit of declarative congruence magic:

https://github.com/gallais/potpourri/blob/b0b734fb8e768f280bc36519048b977b994d1a5e/agda/cong/Syntax/Focus.agda

Unlike the content of Tactic.Cong, it is not trying to guess what the
context should be but instead reads it off the goal type where users can mark the
focus of their action by using the ⟪_⟫ focus.

[JacquesCarette]

Very nice.

A lot of proofs in agda-categories could be made more digestible for humans with such machinery, as quite a lot of work is spent on dealing with cong and re-associating to put a part "in focus". For efficiency, I'd probably want proof-emitting macros rather than using them directly in library code. But that seems most doable. At the level of, say, monoidal categories, such proof-emitting macros might even be a papers' worth of work.

[uncle-betty]

Hello there.

I just opened #2310 without realizing that #2033 existed, which looks more elegant than my hack on top of cong!.

What's the plan going forward with this? Happy to withdraw my proposal, if this is still being worked on.