Sigma assoc

Stream: Is there code for X?

[Anatole Dedecker]

Do we already have something like this ?

def equiv.sigma_assoc {α : Sort*} {β : α → Sort*} {γ : Π (a : α), β a → Sort*} :
  (Σ (ab : Σ (a : α), β a), γ ab.1 ab.2) ≃ Σ (a : α), (Σ (b : β a), γ a b) :=
{ to_fun := λ x, ⟨x.1.1, ⟨x.1.2, x.2⟩⟩,
  inv_fun := λ x, ⟨⟨x.1, x.2.1⟩, x.2.2⟩,
  left_inv := λ ⟨⟨a, b⟩, c⟩, rfl,
  right_inv := λ ⟨a, ⟨b, c⟩⟩, rfl }

[Scott Morrison]

I guess not. It should presumably be in data.equiv.basic.

[Floris van Doorn]

Please replace Sort* by Type* or sigma by psigma (or add two declarations, one for each option)