Proper notion of equivalent types

Stream: new members

[Keefer Rowan]

I am trying to figure out what the proper notion of equivalence of types is w/r/t proving theorems. E.g. it seems like we should be able to say that $(\alpha \times \beta) \to \gamma$ is equivalent to $\alpha \to \beta \to \gamma$ and that $\alpha \times \beta$ is equivalent to $\beta \times \alpha$ (in some sense). Further, it seems we should be able to say mathematically equivalent but distinct definitions of structures should be equivalent in some sense, e.g. defining groups with an existence statement about an inverse (groups1) vs. defining group with an inverse operation (groups2).

Ideally, we want a notion of equivalence which gives us the ability to exchange the types in appropriate circumstances, e.g. taking the example with groups, we should be able to say something like "every theorem about groups1 is a theorem about groups2", but of course this isn't precisely true. What is the right way to think about this problem in the context of formalization: how can we formally say "your definition is the same as mine"?

It is worth noting I asked this question on Math Stack Exchange; more context/examples are given there.

[Matt Earnshaw]

there is a notion of equivalence of types in lean which is simply the type of functions A -> B with two-sided inverse -- you can find the definition and theorems in data.equiv.basic. so for example

variables (A B C : Type)
example : (A × B) ≃ (B × A) := equiv.prod_comm A B
example : (A → B → C) ≃ (A × B → C) := equiv.arrow_arrow_equiv_prod_arrow A B

we can also import tactic.equiv_rw, to rewrite along equalities like so

example (h : A × B) : (B × A) :=
begin
  equiv_rw (equiv.prod_comm A B) at h,
  exact h,
end

now, this can do what we want from equality to some extent, but we can't lift equivalence to equality in general (we do not have univalence in Lean, my understanding is that it would break proof irrelevance). but since we have propext : ∀ {a b : Prop}, (a ↔ b) → a = b (and funext), we can prove things like equality of inductively defined sets, which might cover some of your needs -- see this kata for an example: https://www.codewars.com/kata/5cc47f8c4b8fea001de6d226/lean