English
The dependent product of sorts is associative up to an equivalence: (Σ' ab : Σ' a: α, β a, γ ab.1 ab.snd) ≃ Σ' a: α, Σ' b: β a, γ a b.
Русский
Зависимая произведение видов ассоциативно до эквивалентности: (Σ' ab : Σ' a: α, β a, γ ab.1 ab.snd) ≃ Σ' a: α, Σ' b: β a, γ a b.
LaTeX
$$$${\Sigma' ab : \Sigma' a: α, β a, γ ab.1 ab.snd} \cong \Sigma' a: α, \Sigma' b: β a, γ a b.$$$$
Lean4
/-- The dependent product of sorts is associative up to an equivalence. -/
def pSigmaAssoc {α : Sort*} {β : α → Sort*} (γ : ∀ a : α, β a → Sort*) :
(Σ' 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⟩
