Definition functorRmOp {B C : category} : [B ^op, C ^op] ⟶ [B, C] ^op. Proof. unshelve refine (makeFunctor _ _ _ _). { exact functor_opp. } { intros H I p. exists (λ b, pr1 p b). abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. } { abstract (intros H; now apply (nat_trans_eq (homset_property _))) using _L_. } { abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). } Defined.
Require Import UniMath.MoreFoundations.Tactics.