Equiv version of `function.swap`

Stream: Is there code for X?

[Anatole Dedecker]

Do we have (Π a b, φ a b) ≃ (Π b a, φ a b) (which is docs#function.swap both ways) ? I couldn't find anything in the usual logic/equiv/basic, and library_search seems to agree, but it feels weird that we don't have it

[Yaël Dillies]

Maybe we could bundle docs#matrix.transpose as an equiv using this?

[Eric Wieser]

I think that bundling would lose us notation (and so shouldn't replace transpose)

[Eric Wieser]

But we do already have docs#matrix.transpose_ring_equiv

[Eric Wieser]

(and weaker versions)

[Yaël Dillies]

This works though.

import order.synonym

variables {α : Type*} (a : order_dual α)

#check a.of_dual -- ⇑order_dual.of_dual a : α
#check a.to_dual -- ⇑order_dual.to_dual a : αᵒᵈᵒᵈ

[Eric Wieser]

I'm talking about Mᵀ notation (in the pretty printer)