| > what purpose on god's green earth would be served by introducing univalence directly to haskell? Generally, when I want to reason about tricky data structures, what I do is: (0) Define a set-isomorphic auxiliary type that's easier to analyze, and whose operations are easier to implement, but have worse asymptotic performance. (1) Prove that transporting the operations on the auxiliary type along the isomorphism yield the operations on the original tricky type. I need univalence for this argument to hold water. > (Oh, and furthermore, you realize that fundeps have precisely the same issues in this setting?) Type classes are already Haskell's controlled mechanism for adding ad-hoc polymorphism “without hurting parametricity too much”. I consider it healthier to reuse and extend this mechanism (which is what functional dependencies do) rather than add a second one for exactly the same purpose (type families). > Contrariwise, don't you find it _useful_ that we can have two monoids, say And and Or, which have different `mappend` behaviour? Sure. In ML, I'd just make two structures having the MONOID signature. Haskellers have this wrong idea that the monoid is just the type - it's not! A monoid is a type plus two operations. Same carrier, different operations - different monoids. > Now, can you imagine having that feature and _also_ respecting the idea that set-isomorphic things should be indistinguishable? How? Yes. Acknowledging that an algebraic structure is more than its carrier set. |
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.