drop HasEquiv instance

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jul 5, 2024 · e64bd15 · e64bd15
1 parent f519fc4
commit e64bd15
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v
@@ -371,7 +371,7 @@ Proof.
            f g h).
 Defined.
 
-Definition cat_bincoprod_swap_rec {A : Type} `{HasEquivs A}
+Definition cat_bincoprod_swap_rec {A : Type} `{Is1Cat A}
   `{!HasBinaryCoproducts A} {a b c : A} (f : a $-> c) (g : b $-> c)
   : cat_bincoprod_rec f g $o cat_bincoprod_swap b a $== cat_bincoprod_rec g f
   := @cat_binprod_swap_corec A^op _ _ _ _