Injectivity of quiver.hom.op

Stream: Is there code for X?

[Kevin Buzzard]

Can you edit your post to explain what you're talking about then? Equality of functors is an evil concept so injectivity of a map between functor types is an evil concept.

[Junyan Xu]

The equivalence is (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ (one extra op) at docs#category_theory.functor.op_unop_equiv

[Adam Topaz]

(deleted)

[Adam Topaz]

(deleted)

[Adam Topaz]

Sorry, misread the question. We should have docs#quiver.hom.op_inj (and now that I'm catching up on the later comments, I see that it has already been found!)