{A B C} `{IsGraph A, IsGraph B, IsGraph C} : Fun01 B C -> Fun01 A B -> Fun01 A C := fun G F => Build_Fun01 _ _ (G o F).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Opposite. Require Import WildCat.Equiv. Require Import WildCat.Induced. Require Import WildCat.NatTrans.