From c726a0fe4fa1803d528437415fdd44a1a41278ea Mon Sep 17 00:00:00 2001
From: Patrick Nicodemus <nicodemus@math.wisc.edu>
Date: Thu, 20 Mar 2025 11:20:15 -0400
Subject: [PATCH] Fix deprecation warnings

---
 Adjunction/Hom.v                    |  2 +-
 Adjunction/Natural/Transformation.v |  2 +-
 Structure/End.v                     |  4 ++--
 Structure/Pullback/Limit.v          |  4 ++--
 Theory/Adjunction.v                 |  2 +-
 Theory/Category.v                   | 16 ++++++++--------
 Theory/Functor.v                    |  2 +-
 Theory/Isomorphism.v                |  4 ++--
 8 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/Adjunction/Hom.v b/Adjunction/Hom.v
index 09165131..de477518 100644
--- a/Adjunction/Hom.v
+++ b/Adjunction/Hom.v
@@ -279,4 +279,4 @@ Qed.
 
 End AdjunctionHom.
 
-Arguments Adjunction_Hom {C D} F%functor U%functor.
+Arguments Adjunction_Hom {C D} F%_functor U%_functor.
diff --git a/Adjunction/Natural/Transformation.v b/Adjunction/Natural/Transformation.v
index 05e50fb7..6ddbb092 100644
--- a/Adjunction/Natural/Transformation.v
+++ b/Adjunction/Natural/Transformation.v
@@ -24,7 +24,7 @@ Class Adjunction_Transform := {
 
 End AdjunctionTransform.
 
-Arguments Adjunction_Transform {C D} F%functor U%functor.
+Arguments Adjunction_Transform {C D} F%_functor U%_functor.
 
 Declare Scope adjunction_scope.
 Declare Scope adjunction_type_scope.
diff --git a/Structure/End.v b/Structure/End.v
index c42d0f19..dd427a05 100644
--- a/Structure/End.v
+++ b/Structure/End.v
@@ -14,8 +14,8 @@ Class End `(F : C^op ∏ C ⟶ D) := {
     wedge_map[end_wedge] ∘ u ≈ @wedge_map _ _ _ W x
 }.
 
-Arguments End {_%category _%category} F%functor.
-Arguments end_wedge {_%category _%category} F%functor {_}.
+Arguments End {_%_category _%_category} F%_functor.
+Arguments end_wedge {_%_category _%_category} F%_functor {_}.
 
 Coercion wedge_obj `(F : C^op ∏ C ⟶ D) (E : End F) := @end_wedge _ _ _ E.
 
diff --git a/Structure/Pullback/Limit.v b/Structure/Pullback/Limit.v
index 15db9f87..31d385ae 100644
--- a/Structure/Pullback/Limit.v
+++ b/Structure/Pullback/Limit.v
@@ -12,10 +12,10 @@ Require Import Category.Instance.Roof.
 Generalizable All Variables.
 
 Definition Pullback_Limit {C : Category} (F : Cospan C) := Limit F.
-Arguments Pullback_Limit {_%category} F%functor /.
+Arguments Pullback_Limit {_%_category} F%_functor /.
 
 Definition Pushout_Limit {C : Category} (F : Span C) := Colimit F.
-Arguments Pushout_Limit {_%category} F%functor /.
+Arguments Pushout_Limit {_%_category} F%_functor /.
 
 Program Definition Pullback_to_Universal {C : Category}
         (F : Cospan C) (P : Pullback_Limit F) :
diff --git a/Theory/Adjunction.v b/Theory/Adjunction.v
index b642af96..dbcb5c5e 100644
--- a/Theory/Adjunction.v
+++ b/Theory/Adjunction.v
@@ -248,7 +248,7 @@ Proof. intros; now rewrites. Qed.
 
 End Adjunction.
 
-Arguments Adjunction {C D} F%functor U%functor.
+Arguments Adjunction {C D} F%_functor U%_functor.
 
 Declare Scope adjunction_scope.
 Declare Scope adjunction_type_scope.
diff --git a/Theory/Category.v b/Theory/Category.v
index 186949b3..f87384df 100644
--- a/Theory/Category.v
+++ b/Theory/Category.v
@@ -67,8 +67,8 @@ Delimit Scope object_scope with object.
 Delimit Scope homset_scope with homset.
 Delimit Scope morphism_scope with morphism.
 
-Arguments dom {_%category _%object _%object} _%morphism.
-Arguments cod {_%category _%object _%object} _%morphism.
+Arguments dom {_%_category _%_object _%_object} _%_morphism.
+Arguments cod {_%_category _%_object _%_object} _%_morphism.
 
 Notation "obj[ C ]" := (@obj C%category)
   (at level 0, format "obj[ C ]") : type_scope.
@@ -178,12 +178,12 @@ Proof. split; auto. Qed.
 
 End Category.
 
-Arguments dom {_%category _%object _%object} _%morphism.
-Arguments cod {_%category _%object _%object} _%morphism.
-Arguments id_left {_%category _%object _%object} _%morphism.
-Arguments id_right {_%category _%object _%object} _%morphism.
-Arguments comp_assoc {_%category _%object _%object _%object _%object}
-  _%morphism _%morphism _%morphism.
+Arguments dom {_%_category _%_object _%_object} _%_morphism.
+Arguments cod {_%_category _%_object _%_object} _%_morphism.
+Arguments id_left {_%_category _%_object _%_object} _%_morphism.
+Arguments id_right {_%_category _%_object _%_object} _%_morphism.
+Arguments comp_assoc {_%_category _%_object _%_object _%_object _%_object}
+  _%_morphism _%_morphism _%_morphism.
 
 #[export]
 Program Instance hom_preorder {C : Category} : PreOrder (@hom C) := {
diff --git a/Theory/Functor.v b/Theory/Functor.v
index 29f04219..8c2a5726 100644
--- a/Theory/Functor.v
+++ b/Theory/Functor.v
@@ -45,7 +45,7 @@ Notation "C ⟶ D" := (@Functor C%category D%category)
   (at level 90, right associativity) : functor_type_scope.
 
 Arguments fmap
-  {C%category D%category Functor%functor x%object y%object} f%morphism.
+  {C%_category D%_category Functor%_functor x%_object y%_object} f%_morphism.
 
 Infix "<$>" := fmap
   (at level 29, left associativity, only parsing) : morphism_scope.
diff --git a/Theory/Isomorphism.v b/Theory/Isomorphism.v
index 5cb5fcf1..d6179ba7 100644
--- a/Theory/Isomorphism.v
+++ b/Theory/Isomorphism.v
@@ -144,8 +144,8 @@ Notation "x ≅ y" := (@Isomorphism _%category x%object y%object)
 Notation "x ≅[ C ] y" := (@Isomorphism C%category x%object y%object)
   (at level 91, only parsing) : isomorphism_scope.
 
-Arguments to {_%category x%object y%object} _%morphism.
-Arguments from {_%category x%object y%object} _%morphism.
+Arguments to {_%_category x%_object y%_object} _%_morphism.
+Arguments from {_%_category x%_object y%_object} _%_morphism.
 Arguments iso_to_from {_ _ _} _.
 Arguments iso_from_to {_ _ _} _.