{A B C : Type} {F G : B -> C} `{IsGraph A, Is1Cat B, Is1Cat C, !Is0Functor F, !Is0Functor G} (alpha : NatTrans F G) (K : A -> B) `{!Is0Functor K} : NatTrans (F o K) (G o K) := Build_NatTrans (trans_prewhisker alpha K) _.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.