Quiver.Hom.unmop_inj

theorem Quiver.Hom.unmop_inj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᴹᵒᵖ}, Function.Injective Quiver.Hom.unmop := by sorry

The theorem `Quiver.Hom.unmop_inj` states that for all categories `C`, and for any two objects `X` and `Y` in the opposite category `Cᴹᵒᵖ`, the function `Quiver.Hom.unmop` is injective. This means that if two morphisms from `X` to `Y` in the opposite category `Cᴹᵒᵖ` are mapped to the same morphism in the original category `C` when we apply the function `Quiver.Hom.unmop` to them, then they must have been the same morphism in the opposite category `Cᴹᵒᵖ` to begin with.

More concisely: Given any categories C and for any objects X and Y in Cᴹᵒᵖ, the function Quiver.Hom.unmop maps distinct morphisms from X to Y in Cᴹᵒᵖ to distinct morphisms in C.