English
There is an extensionality principle for equalizers in a Trident: if two arrows k, l into the apex satisfy k ≫ ι = l ≫ ι, then they are equal after projecting to any component j.
Русский
Существует принцип экстентности для эквалайзера в триденте: если две стрелки k, l в вершину апекса удовлетворяют k ≫ ι = l ≫ ι, то они равны после проекции на любой компонент j.
LaTeX
$$$\exists j : WalkingParallelFamily J,\ k \circ s.ι = l \circ s.ι \Rightarrow \forall j,\ k ≫ s.π.app j = l ≫ s.π.app j$$$
Lean4
/-- To check whether two maps are equalized by both maps of a trident, it suffices to check it for
the first map -/
theorem equalizer_ext [Nonempty J] (s : Trident f) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
∀ j : WalkingParallelFamily J, k ≫ s.π.app j = l ≫ s.π.app j
| zero => h
| one => by rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]
