Lemma is_right_adjoint_opposite' {C D : category} (F : functor C D) : is_left_adjoint (functor_op F) -> is_right_adjoint F. Proof. intro ila. apply (is_right_adjoint_opposite (functor_op F) ila). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.OppositeCategory.Core.