From e64bd157b22bf55ade322328e154e8d543805003 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 5 Jul 2024 18:48:35 +0200 Subject: [PATCH] drop HasEquiv instance Signed-off-by: Ali Caglayan --- theories/WildCat/Coproducts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v index f953994ca54..fb0ab2fe1aa 100644 --- 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 _ _ _ _