[sclv]

> I need univalence for this argument to hold water.

No, you don't. Univalence is the axiom that transporting operations across such equivalences _always_ works. If you're doing equational reasoning directly it doesn't arise.

Furthermore, all you need to do is to establish that the _type operations_ regarding one type respect the equivalence to the other type as an additional step.

As you say "a monoid is a type plus two operations" -- so fine, we can treat the monoid And as the type bool and the dictionary of operations on it, and all this still works out.

[catnaroek]

> No, you don't. Univalence is the axiom that transporting operations across such equivalences _always_ works.

Sure, but the strategy I outlined is risky (as in “may lead to getting suck and having to undo work”) in a language where this isn't guaranteed to work.

> As you say "a monoid is a type plus two operations" -- so fine, we can treat the monoid And as the type bool and the dictionary of operations on it, and all this still works out.

Yup, but Haskell doesn't let you define types parameterized by entire algebraic structures. It only lets you define types parameterized by the carriers of algebraic structures.