English
Given two index families A : α → PSet and B : β → PSet with an elementwise equivalence A(a) ≃ B(b) compatible with a relation α → ∃ b, the corresponding fibers of the two sUnion constructions are equivalent for appropriate indices.
Русский
Для двух семейств индексов A и B существование попарных эквивалентностей между соответствующими элементами порождает эквивалентность соответствующих волокон при операции объединения по множеству.
LaTeX
$$$ \forall a, \exists b, ((sUnion \langle \alpha, A \rangle).Func a) \cong ((sUnion \langle \beta, B \rangle).Func b) $$$
Lean4
theorem sUnion_lem {α β : Type u} (A : α → PSet) (B : β → PSet) (αβ : ∀ a, ∃ b, Equiv (A a) (B b)) :
∀ a, ∃ b, Equiv ((sUnion ⟨α, A⟩).Func a) ((sUnion ⟨β, B⟩).Func b)
| ⟨a, c⟩ => by
let ⟨b, hb⟩ := αβ a
induction ea : A a with
| _ γ Γ
induction eb : B b with
| _ δ Δ
rw [ea, eb] at hb
obtain ⟨γδ, δγ⟩ := hb
let c : (A a).Type := c
let ⟨d, hd⟩ := γδ (by rwa [ea] at c)
use ⟨b, Eq.ndrec d (Eq.symm eb)⟩
change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))
match A a, B b, ea, eb, c, d, hd with
| _, _, rfl, rfl, _, _, hd => exact hd
