Library UniMath.CategoryTheory.OppositeCategory.Core

Require Import UniMath.Foundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.

Require Import UniMath.CategoryTheory.opp_precat.

Definition opp_cat (C : category)
  : category.
Show proof.

Notation " C ^opp" := (opp_cat C) (at level 31).

Definition functor_op {C D : category} (F : functor C D)
  : functor (opp_cat C) (opp_cat D)
  := functor_opp F.