Conflicts in notations with Coq 8.19

[jjhugues]

Lib/Foundation.v defines notations for ∀ , ∃, and λ

If user code imports both Category.Lib and Utf8 from the Coq standard library, we get the following error message

Error: Notation "∀ _ .. _ , _" is already defined at level 200 with arguments
binder, constr at level 200 while it is now required to be at level 10
with arguments binder, constr at level 200.

The following patch seems enough to work around this issue: I confirmed category-theory compiles and so does my code. Before proposing a pull request, I am curious about your feedback on this. I must admit my patch is pretty arbitrary, it ressembles the notation definition from the Coq standard library to avoid conflicts.

diff --git a/Lib/Foundation.v b/Lib/Foundation.v
index 82f7455..560a8c2 100644
--- a/Lib/Foundation.v
+++ b/Lib/Foundation.v
@@ -31,7 +31,7 @@ Arguments Basics.arrow _ _ /.
 Arguments Datatypes.id {_} _ /.
 
 Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, P at level 200, right associativity) :
   category_theory_scope.
 
 Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
@@ -40,7 +40,7 @@ Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
   category_theory_scope.
 
 Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, P at level 200, right associativity) :
   category_theory_scope.
 
 Notation "x → y" := (x -> y)
@@ -55,5 +55,5 @@ Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
 Infix "∨" := sum (at level 85, right associativity) : category_theory_scope.
 
 Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, t at level 200, right associativity) :
   category_theory_scope.

Thanks,

[jjhugues]

@jwiegley would you welcome a PR on this or is there anything you want to check first?

[jwiegley]

If this passes our CI, I'd happily accept such a PR, thank you.

[jwiegley]

@jjhugues Would you be willing to submit that PR? Happy to merge it.

[jjhugues]

Sorry it sat on my repo for so long.

[jwiegley]

No worries! I'm grateful for the work, whenever it gets in. :)