(A B : Type) `{IsGraph A} `{IsGraph B} : _ <~> Fun01 A B := ltac:(issig). Global Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B). Proof. srapply Build_IsGraph. intros [F ?] [G ?]. exact (NatTrans F G). 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.