{A B C D : Type} `{IsGraph A, HasEquivs B, HasEquivs C, HasEquivs D} (F : C -> D) (G : B -> C) (K : A -> B) `{!Is0Functor F, !Is0Functor G, !Is0Functor K} : NatEquiv ((F o G) o K) (F o (G o K)). Proof. snrapply Build_NatEquiv. 1: intro; reflexivity. snrapply Build_Is1Natural. intros X Y f. refine (cat_prewhisker (id_cate_fun _) _ $@ cat_idl _ $@ _^$). refine (cat_postwhisker _ (id_cate_fun _) $@ cat_idr _). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.