{B C : Type} `{Is1Cat B, Is1Gpd C} `{IsPointed B, IsPointed C} {F0 F1 F2 : B -->* C} : (F0 $=>* F1) -> (F1 $=>* F2) -> (F0 $=>* F2). Proof. intros [h0 p0] [h1 p1]. exists (trans_comp h1 h0). refine ((p1 $@R _) $@ (_ $@L p0) $@ _); unfold gpd_comp; cbn. refine (cat_assoc _ _ _ $@ _). rapply (fmap _). apply gpd_h_Vh. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.