agda
Generalise fold-fusion results
Cf. this blog post by @oisdk
We’re not using the proofs in Agda’s standard library because these are tied to propositional equality. In other words, instead of using an abstract binary relation, they prove things over actual equality. That’s all well and good, but as you can see above, we don’t need propositional equality: we don’t even need the relation to be an equivalence, we just need transitivity and reflexivity.
Well, we now (PR #1668) have some more systematic ≡-based fold*-fusion results in Data.Vec.Properties (and soon, some more heterogeneous ones about reverse to go... somewhere), so part of that reconsideration might be to generalise these things.
One day.
