{A B C} {H K : B -> C} `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor H, !Is0Functor K} (alpha : NatEquiv H K) (F : A -> B) `{!Is0Functor F} : NatEquiv (H o F) (K o F) := Build_NatEquiv' (nattrans_prewhisker alpha F).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.