{A : Type} `{Is21Cat A} {a b c : A} {f f' f'' : a $-> b} {g g' g'' : b $-> c} (p : f $== f') (q : f' $== f'') (r : g $== g') (s : g' $== g'') : (p $@ q) $@@ (r $@ s) $== (p $@@ r) $@ (q $@@ s). Proof. unfold "$@@". nrefine ((_ $@L cat_prewhisker_pp _ _ _ ) $@ _). nrefine ((cat_postwhisker_pp _ _ _ $@R _) $@ _). nrefine (cat_assoc _ _ _ $@ _). refine (_ $@ (cat_assoc _ _ _)^$). nrefine (_ $@L _). refine (_ $@ cat_assoc _ _ _). refine ((cat_assoc _ _ _)^$ $@ _). nrefine (_ $@R _). apply bifunctor_coh_comp. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.NatTrans.