English
Let P be a presheaf of types on a category C. For any morphism f: X → B and any pair of arrows g1, g2: W → X with g1 ∘ f = g2 ∘ f, there is a canonical map from P(B) to the equalizer object consisting of those elements x ∈ P(X) for which P.map g1.op x = P.map g2.op x. This map sends t ∈ P(B) to P.map f.op t together with a certificate that P.map g1.op (P.map f.op t) = P.map g2.op (P.map f.op t).
Русский
Пусть P — префунктор над C в типах. Пусть f: X → B, g1, g2: W → X удовлетворяют g1 ∘ f = g2 ∘ f. Тогда существует каноническое отображение P(B) → {x ∈ P(X) | P.map g1.op x = P.map g2.op x}, отправляющее t ∈ P(B) в P.map f.op t, вместе с доказательством несогласованности P.map g1.op (P.map f.op t) = P.map g2.op (P.map f.op t).
LaTeX
$$$ MapToEqualizer\\; (P : C^{\\mathrm{op}} \\to Type^*) \\; (f : X \\to B) \\; (g_1,g_2 : W \\to X) \\; (w : g_1 \\; f = g_2 \\; f) \\, : \\, P( op B ) \\to \\{ x : P(op X) \\; | \\; P.map g_1.op x = P.map g_2.op x \\} \\\\ t \\mapsto \\langle P.map f.op t, \\; P.map g_1.op (P.map f.op t) = P.map g_2.op (P.map f.op t) \\rangle$$
Lean4
/-- The canonical map to the explicit equalizer. -/
def MapToEqualizer (P : Cᵒᵖ ⥤ Type*) {W X B : C} (f : X ⟶ B) (g₁ g₂ : W ⟶ X) (w : g₁ ≫ f = g₂ ≫ f) :
P.obj (op B) → {x : P.obj (op X) | P.map g₁.op x = P.map g₂.op x} := fun t ↦
⟨P.map f.op t, by simp only [Set.mem_setOf_eq, ← FunctorToTypes.map_comp_apply, ← op_comp, w]⟩
