{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. intros [a n]. snrapply Build_NatEquiv. 1: exact a. by rapply is1natural_op. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.