fact: Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B} {ff : Is0Functor F} {fg : Is0Functor G} := { trans_nattrans : F $=> G ; is1natural_nattrans : Is1Natural F G trans_nattrans ; }.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Square