{A B C} `{Is1Cat A, Is1Cat B, Is1Cat C} : Fun11 B C -> Fun11 A B -> Fun11 A C. Proof. intros F G. nrapply Build_Fun11. rapply (is1functor_compose G F). Defined.
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.