fact: Definition opposite_functor_law 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.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Dual Functor.Dual NaturalTransformation.Dual Functor.Identity FunctorCategory.Core Functor.Paths HoTT.Tactics