{A B C} {F G : A -> B} `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor F, !Is0Functor G} (K : B -> C) (alpha : NatEquiv F G) `{!Is0Functor K, !Is1Functor K} : NatEquiv (K o F) (K o G). Proof. srefine (Build_NatEquiv' (nattrans_postwhisker K alpha)). 2: unfold nattrans_postwhisker, trans_postwhisker; cbn. all: exact _. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.