CategoryTheory.LocallyDiscrete.eq_of_hom

theorem CategoryTheory.LocallyDiscrete.eq_of_hom : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X Y : CategoryTheory.LocallyDiscrete C} {f g : X ⟶ Y}, (f ⟶ g) → f = g

The theorem `CategoryTheory.LocallyDiscrete.eq_of_hom` states that for any locally discrete category `C` with two objects `X` and `Y`, if there exist two morphisms `f` and `g` from `X` to `Y`, any 2-morphism from `f` to `g` implies that `f` is equal to `g`. In other words, in a locally discrete 2-category, any 2-morphism can be extracted as an equality of the morphisms it connects.

More concisely: In a locally discrete 2-category, any 2-isomorphism between morphisms is an equality.