{A} `{Is21Cat A} {a b c : A} {f g h : a $-> b} (k : b $-> c) (p : f $== g) (q : g $== h) : k $@L (p $@ q) $== (k $@L p) $@ (k $@L q). Proof. rapply fmap_comp. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.NatTrans.