C D : opposite_functor C D o (opposite_functor C^op D^op)^op = 1 /\ (opposite_functor C^op D^op)^op o opposite_functor C D = 1. Proof. op_t C D. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual Functor.Dual NaturalTransformation.Dual. Require Import Functor.Identity. Require Import FunctorCategory.Core. Require Import Functor.Paths. Require Import HoTT.Tactics.