Skip to content

Commit

Permalink
Removed accidental code
Browse files Browse the repository at this point in the history
  • Loading branch information
patrick-nicodemus committed Jan 26, 2025
1 parent 0ea00ce commit cf3f88e
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions theories/WildCat/NatTrans.v
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down

0 comments on commit cf3f88e

Please sign in to comment.