Merge pull request #2012 from Alizter/ps/rr/rename_opposite_initial_t…

…erminal_instances rename opposite initial/terminal instances
HoTT · Jul 4, 2024 · d1ffba6 · d1ffba6
2 parents ef10640 + e28fbfa
commit d1ffba6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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.