English
If F(a): β1(a) ≃ β2(a) and G(a): β2(a) ≃ β3(a) are fiberwise equivalences, then the composition yields an equivalence between Σ' a, β1(a) and Σ' a, β3(a): (psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight (λ a, (F(a)).trans (G(a))).
Русский
Пусть для каждого a дано эквивалентность F(a): β1(a) ≃ β2(a) и G(a): β2(a) ≃ β3(a). Тогда композиция даёт эквивалентность между Σ'a, β1(a) и Σ'a, β3(a): (psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight (λ a, (F(a)).trans (G(a))).
LaTeX
$$$$(psigmaCongrRight F).\text{trans}(psigmaCongrRight G) = psigmaCongrRight (\lambda a. (F a).trans (G a)).$$$$
Lean4
theorem psigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
(psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight fun a => (F a).trans (G a) :=
rfl
