Definition opp_cat (C : category) : category. Proof. exists (opp_precat C). apply has_homsets_op. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat.