English
The dependent product of types is associative up to an equivalence: (Σ ab : Σ a, β a, γ ab.1 ab.2) ≃ Σ a, Σ b, γ a b.
Русский
Зависимая сумма типов ассоциативна до эквивалентности: (Σab : Σa, β a, γ ab.1 ab.2) ≃ Σ a, Σ b, γ a b.
LaTeX
$$$${\Sigma ab : Σ a:\alpha, \beta a, \gamma( ab.1, ab.2 )} \cong \Sigma a: \alpha, \Sigma b: \beta a, \gamma a b.$$$$
Lean4
/-- The dependent product of types is associative up to an equivalence. -/
def sigmaAssoc {α : Type*} {β : α → Type*} (γ : ∀ a : α, β a → Type*) :
(Σ ab : Σ a : α, β a, γ ab.1 ab.2) ≃ Σ a : α, Σ b : β a, γ a b
where
toFun x := ⟨x.1.1, ⟨x.1.2, x.2⟩⟩
invFun x := ⟨⟨x.1, x.2.1⟩, x.2.2⟩
