Merge pull request #2017 from Alizter/ps/rr/drop_hasequiv_instance

drop HasEquiv instance
HoTT · Jul 5, 2024 · bca6381 · bca6381
2 parents f519fc4 + e64bd15
commit bca6381
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 _ _ _ _