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