category_theory.has_hom.opposite

The hom types of the opposite of a category (or graph).

As with the objects, we'll make this irreducible below. Use f.op and f.unop to convert between morphisms of C and morphisms of Cᵒᵖ.