eq_of_hom — Mathlib

English

In LocallyDiscrete C, a 2-morphism η: f ⟶ g determines the equality f = g.

Русский

В LocallyDiscrete C 2-морфизм η: f ⟶ g определяет равенство f = g.

LaTeX

$$$\\forall X,Y:\\text{LocallyDiscrete } C, \\forall f,g:\\, X ⟶ Y, \\forall η:\\, f\\to g,\\; f = g.$$$

Lean4

/-- Extract the equation from a 2-morphism in a locally discrete 2-category. -/
theorem eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f = g :=
  Discrete.ext η.1.1

Похожие утверждения