Homotopy Type Theory opposite precategory > history (Rev #2, changes)

The opposite precategory is the precategory obtained by reversing the directions of the arrows.

Definition

For a precategory $A$, its opposite $A^{op}$ is a precategory with the same type of objects, with $hom_{A^{op}}(a,b)\equiv hom_A(b,a)$, and with identities and composition inherited from $A$.

See also

Category theory precategory yoneda lemma

References

HoTT book