Zulip Chat Archive

Stream: general

Topic: generalize relations to α → α → Sort


Yaël Dillies (Jun 15 2021 at 10:23):

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 (Jun 15 2021 at 10:24):

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

Yaël Dillies (Jun 15 2021 at 10:42):

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 (Jun 15 2021 at 12:38):

docs#is_symm_op

Yaël Dillies (Jun 15 2021 at 12:43):

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 (Jun 15 2021 at 12:47):

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 (Jun 15 2021 at 12:48):

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 (Jun 15 2021 at 12:49):

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

Yakov Pechersky (Jun 15 2021 at 12:50):

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.


Last updated: Dec 20 2023 at 11:08 UTC