{A B : Type} `{IsGraph A} `{HasEquivs B} {F : A -> B} `{!Is0Functor F} : NatEquiv F F := Build_NatEquiv' (nattrans_id F).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.