From e28fbfaa9786a5cdcda15891d616f66c5f4c3850 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 4 Jul 2024 14:55:17 +0200 Subject: [PATCH] rename opposite initial/terminal instances Signed-off-by: Ali Caglayan --- theories/WildCat/Opposite.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v index 1c515862c38..8d26289d5bf 100644 --- a/theories/WildCat/Opposite.v +++ b/theories/WildCat/Opposite.v @@ -127,10 +127,10 @@ Proof. refine (@isequiv_Htpy_path _ _ _ _ _ H0 b a f g). Defined. -Global Instance isinitial_isterminal_op {A : Type} `{Is1Cat A} (x : A) +Global Instance isinitial_op_isterminal {A : Type} `{Is1Cat A} (x : A) {t : IsTerminal x} : IsInitial (A := A^op) x := t. -Global Instance isterminal_isinitial_op {A : Type} `{Is1Cat A} (x : A) +Global Instance isterminal_op_isinitial {A : Type} `{Is1Cat A} (x : A) {i : IsInitial x} : IsTerminal (A := A^op) x := i.