diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v index 28b00c509c..eb47b3c164 100644 --- a/theories/WildCat/NatTrans.v +++ b/theories/WildCat/NatTrans.v @@ -176,8 +176,6 @@ Arguments Build_NatTrans {A B isgraph_A isgraph_B is2graph_B is01cat_B is1cat_B Global Existing Instance is1natural_nattrans. -Hint Mode is1natural_nattrans - - - - - - - - - - + + : typeclass_instances. - Definition issig_NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} (F G : A -> B) {ff : Is0Functor F} {fg : Is0Functor G} : _ <~> NatTrans F G := ltac:(issig).