generalize relations to α → α → Sort

Stream: general

[Yaël Dillies]

Say I have a function f : α → α → β and I proved that ∀ x y, f x y = f y x. I now want to lift it to a function g : sym2 α → β so I use sym2.from_rel. But wait! sym2.from_rel is only defined for functions α → α → Prop. And now I'm annoyed.

Of course Prop-valued functions have nothing special in that context (and for now I've copy-pasted the definition of sym2.from_rel for my purposes and it works just fine), so what about we generalize it?
The problem is that sym2.from_rel uses symmetric r, and that is also only defined for Prop-valued functions. Is there any equivalent for Type-valued functions? Note that symmetric is currently very Prop-specific as it is an implication, not an equality.

[Yaël Dillies]

commutative is a good candidate, but it's in the core and is about functions α → α → α for no reason.

[Yaël Dillies]

If I generalise def commutative {α : Type u} {β : Sort v} (f : α → α → β) : Prop, I think everything goes fine and we can even prove stuff live symmetric iff commutative. Any objections?

[Yakov Pechersky]

docs#is_symm_op

[Yaël Dillies]

Oh wow, that's quite nice! But still not enough. I want β : Sort v as otherwise I'll have to duplicate code for sym2.from_rel.

[Yakov Pechersky]

I don't understand why you have to use sym2.from_rel. Isn't what you want just a quotient.lift? The proof that it lifts into the quotient is so simple, that the duplication, I think, is fine.

[Yakov Pechersky]

sym2.from_rel is special because it's doing two things, it's lifting a relationship and also using defeq to turn it into a creation of a set.

[Yakov Pechersky]

In your case, you're just lifting the function.

[Yakov Pechersky]

You can generalize is_symm_op, basically nothing uses it (I think I've made the sole mathlib instance of it). But there might be some issues with out_param into Sort (or Prop), not sure.