English
A sigma of a sigma where the second base does not depend on the first is equivalent to a sigma whose base is a product.
Русский
Сигма-тип над сигма-типом, где вторая база не зависит от первой, эквивалентен сигма-типу с базой в виде произведения.
LaTeX
$$$\\left( (ab : \\alpha \\times \\beta) \\times \\gamma\\ ab.1\\ ab.2 \\right) \\simeq (a : \\alpha) \\times (b : \\beta) \\times \\gamma a b$$$
Lean4
/-- A sigma of a sigma whose second base does not depend on the first is equivalent
to a sigma whose base is a product. -/
@[simps!]
def sigmaAssocProd {α β : Type*} {γ : α → β → Type*} : (ab : α × β) × γ ab.1 ab.2 ≃ (a : α) × (b : β) × γ a b :=
sigmaCongrLeft' (sigmaEquivProd _ _).symm |>.trans <| sigmaAssoc γ
