fact: Definition fun01_postcomp {A B C} `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C) : Fun01 A B -> Fun01 A C := fun01_compose (A:=A) F.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Induced WildCat.NatTrans