English
A universe-varying version: mk_sigma_congr' states that the equality of fiber sizes under an equivalence yields equality of the corresponding sigma-types across universes.
Русский
Версия с изменением вселенной: mk_sigma_congr' говорит, что равенство размеров волокон при эквивалентности порождает равенство соответствующих сигма-типов между вселенными.
LaTeX
$$$\forall {\iota : Type u} {\iota' : Type v} {f : \iota → Type w} {g : \iota' → Type w}, (e : Equiv ι ι')\Rightarrow (∀ i, |f i| = |g(e i)|) \Rightarrow |Σ i, f i| = |Σ i, g i|$$$
Lean4
/-- Similar to `mk_sigma_congr` with indexing types in different universes. This is not a strict
generalization. -/
theorem mk_sigma_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)} {g : ι' → Type max w (max u v)}
(e : ι ≃ ι') (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i) :=
mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)
