punchOut preserves ordering

[Taneb]

No description provided.

[jamesmckinna]

These all look plausible/reasonable (and contribute to your ongoing investigation of Permutation{.TranspositionList}), but I can't help... wondering... if writing down the function-graph view of punchIn and punchOut might not provide a (better?) 'shrink-wrapped' approach to lemmas of this kind (and their many friends in the library), precisely by encapsulating in one place all and only the pattern analyses relevant to the computational behaviour/call-graph of the functions.

[Taneb]

@jamesmckinna I'm afraid I don't know what you mean by "function-graph view" here. As it seems like it's off-topic to the question of whether to merge this PR in the immediate term, could I ask you to message me on Zulip about it?

[jamesmckinna]

@Taneb happy to take the discussion elsewhere, but I'm not at all sure it's off topic. But I'll let you make that judgment.

[jamesmckinna]

For definiteness, I'd sent a preliminary version of the PunchOut one of these to @Taneb
but I'd happily raise a (competing, sorry) PR for these three views of the corresponding functions, with the corresponding properties derived, if there were interest in further discussion. Oh, GitHib doesn't support drag-and-drop of filetype .agda... so I'll make a branch... here
See PR #1921