English
If two index types J and J′ are equivalent via an equivalence h : J ≃ J′, then the corresponding wide pushout shapes are equivalent as categories; i.e., WidePushoutShape J and WidePushoutShape J′ are categorically equivalent.
Русский
Если два индекса J и J′ эквивалентны через эквивалентность h : J ≃ J′, то соответствующие формы широкого объединения эквивалентны как категории; то есть WidePushoutShape J эквивалентна WidePushoutShape J′.
LaTeX
$$$\\mathrm{WidePushoutShape}(J) \\simeq \\mathrm{WidePushoutShape}(J')\\quad$за условиям существования эквивалентности $h : J \\simeq J'$.$$
Lean4
/-- Wide pushout diagrams of equivalent index types are equivalent. -/
def equivalenceOfEquiv (J' : Type w') (h : J ≃ J') : WidePushoutShape J ≌ WidePushoutShape J'
where
functor := wideSpan none (fun j => some (h j)) fun j => Hom.init (h j)
inverse := wideSpan none (fun j => some (h.invFun j)) fun j => Hom.init (h.invFun j)
unitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))
counitIso := NatIso.ofComponents (fun j => by cases j <;> exact eqToIso (by simp))
