Isomorphic products

Stream: lean4

[Kind Bubble]

Sometimes annoying differences between isomorphic products arise:

variable {A : Type}
variable {B : Type}
variable {C : Type}
def X := (A × B) × C
def Y := A × (B × C)

It would be nice if there were a way of handling these different isomorphic products.

[Jireh Loreaux]

There's docs#equiv.prod_assoc. Is that what you're looking for?

[Adam Topaz]

There are various ways of going back and forth, but you should explain what you mean by "handle" more precisely.

[Trebor Huang]

I recall a no-go theorem in category theory, that basically says these two cannot be judgementally equal, unless you have very bizzare type theories.