{A B : Type} `{IsGraph A} `{HasEquivs B} {F G : A -> B} `{!Is0Functor F, !Is0Functor G} : NatEquiv F G -> NatEquiv G F. Proof. intros [alpha I]. snrapply Build_NatEquiv. 1: exact (fun a => (alpha a)^-1$). snrapply Build_Is1Natural'. + intros X Y f. apply vinverse, I. + intros X Y f. apply hinverse, I. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.