{A B : Type} `{Is01Cat A} `{Is1Cat B} {F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G} {alpha : F $=> G} (gamma : F $=> G) `{!Is1Natural F G gamma} (p : forall a, alpha a $== gamma a) : Is1Natural F G alpha. Proof. snrapply Build_Is1Natural. intros a b f. exact ((p b $@R _) $@ isnat gamma f $@ (_ $@L (p a)^$)). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.