{A B C} `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C) : Fun01 A B -> Fun01 A C := fun01_compose (A:=A) F. Global Instance is0functor_fun01_postcomp {A B C} `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C) : Is0Functor ( (A:=A) F). Proof. apply Build_Is0Functor. intros a b f. rapply nattrans_postwhisker. exact 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.