proposition: Lemma natequiv_op {A B : Type} `{Is01Cat A} `{HasEquivs B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} : NatEquiv F G -> NatEquiv (G : A^op -> B^op) F.
proof: Proof. intros [a n]. snrapply Build_NatEquiv. { intro x. exact (a x). } rapply is1nat_op. Defined.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.NatTrans WildCat.FunctorCat