English
An auxiliary equivalence identifies sections of a multicospan (once forgotten) with tuples of elements in the left objects satisfying all right-hand identicalities across the multicospan.
Русский
Вспомогательное эквивалентное отображение переводит секции multicospan (после забывания) в кортежи элементов левых объектов с выполнением всех правых равенств на multicospan.
LaTeX
$$$\\text{multiequalizerEquivAux} : (I.multicospan \\downarrow forget\\ C)\\text{-sections} \\simeq \\{ x : \\forall i : J.L, ToType(I.left i) \\mid \\forall i : J.R, I.fst i (x _) = I.snd i (x _) \\}$$$
Lean4
theorem widePullback_ext {B : C} {ι : Type w} {X : ι → C} (f : ∀ j : ι, X j ⟶ B) [HasWidePullback B X f]
[PreservesLimit (wideCospan B X f) (forget C)] (x y : ToType (widePullback B X f)) (h₀ : base f x = base f y)
(h : ∀ j, π f j x = π f j y) : x = y := by
apply Concrete.limit_ext
rintro (_ | j)
· exact h₀
· apply h
