{A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : F $=> G) (isnat : forall a a' (f : a $-> a'), alpha a' $o fmap F f $== fmap G f $o alpha a) : Is1Natural F G alpha. Proof. snrapply '. - exact isnat. - intros a a' f. exact (isnat a a' f)^$. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.