Merge pull request #134 from herbelin/master+closed-notation-level-0

Construction/Comma/Adjunction.v

@@ -56,7 +56,7 @@ Context {G : C ⟶ D}.
 Definition πD := comma_proj1.
 Definition πC := comma_proj2.
 
-#[local] Notation "⟨πD,πC⟩" := comma_proj (at level 100).
+#[local] Notation "⟨πD,πC⟩" := comma_proj (at level 0).
 
 Record lawvere_equiv := {
   lawvere_iso : F ↓ Id[C] ≅[Cat] Id[D] ↓ G;

Functor/Applicative.v

@@ -36,4 +36,4 @@ Arguments Applicative {_ _} F.
 Arguments pure {C _ F _ _ _}.
 
 Notation "pure[ F ]" := (@pure _ _ F _ _ _)
-  (at level 9, format "pure[ F ]") : morphism_scope.
+  (at level 0, format "pure[ F ]") : morphism_scope.

Functor/Diagonal.v

@@ -26,12 +26,12 @@ Program Instance Diagonal_Product `(C : Category) : C ⟶ C ∏ C.
 
 End Diagonal_Product.
 
-Notation "Δ[ J ]( c )" := (Diagonal J c) (at level 90, format "Δ[ J ]( c )") : functor_scope.
+Notation "Δ[ J ]( c )" := (Diagonal J c) (at level 0, format "Δ[ J ]( c )") : functor_scope.
 
 Require Import Category.Instance.One.
 
-Notation "Δ( c )" := (Diagonal _ c) (at level 90, format "Δ( c )") : functor_scope.
-Notation "=( c )" := (Diagonal 1 c) (at level 90, format "=( c )") : functor_scope.
+Notation "Δ( c )" := (Diagonal _ c) (at level 0, format "Δ( c )") : functor_scope.
+Notation "=( c )" := (Diagonal 1 c) (at level 0, format "=( c )") : functor_scope.
 
 Definition Δ {C J : Category} := @Diagonal C J.
 

Functor/Product/Internal.v

@@ -25,4 +25,4 @@ Next Obligation.
 Qed.
 
 Notation "×( C )" := (@InternalProductFunctor C _)
-  (at level 90, format "×( C )") : functor_scope.
+  (at level 0, format "×( C )") : functor_scope.

Functor/Structure/Monoidal/Pure.v

@@ -53,4 +53,4 @@ End Pure.
 Arguments pure {C _ F _ _ A}.
 
 Notation "pure[ F ]" := (@pure _ _ F _ _ _)
-  (at level 9, format "pure[ F ]") : morphism_scope.
+  (at level 0, format "pure[ F ]") : morphism_scope.

Instance/Cones/Limit.v

@@ -11,7 +11,7 @@ Program Definition Limit_Cones `(F : J ⟶ C) `{T : @Terminal (Cones F)} :
   Limit F := {|
   limit_cone := @terminal_obj _ T;
   ump_limits := fun N =>
-    {| unique_obj := `1 @one _ T N
-     ; unique_property := `2 @one _ T N
+    {| unique_obj := `1 (@one _ T N)
+     ; unique_property := `2 (@one _ T N)
      ; uniqueness       := fun v H => @one_unique _ T N (@one _ T N) (v; H) |}
 |}.

Instance/Coq/Applicative.v

@@ -35,11 +35,11 @@ Arguments ap   {F _ _ _} _ x.
 
 Coercion Applicative_Functor `{@Applicative F} : Coq ⟶ Coq := F.
 
-Notation "pure[ F ]" := (@pure F _ _) (at level 19, F at next level).
-Notation "pure[ F G ]" := (@pure (fun x => F (G x)) _ _) (at level 9).
+Notation "pure[ F ]" := (@pure F _ _) (at level 0, F at next level).
+Notation "pure[ F G ]" := (@pure (fun x => F (G x)) _ _) (at level 0).
 
-Notation "ap[ F ]" := (@ap F _ _ _) (at level 9).
-Notation "ap[ F G ]" := (@ap (fun x => F (G x)) _ _ _) (at level 9).
+Notation "ap[ F ]" := (@ap F _ _ _) (at level 0).
+Notation "ap[ F G ]" := (@ap (fun x => F (G x)) _ _ _) (at level 0).
 
 Infix "<*>" := ap (at level 29, left associativity).
 Notation "x <**> F" := (ap F x) (at level 29, left associativity).

Theory/Coq/Applicative.v

@@ -28,16 +28,16 @@ Module ApplicativeNotations.
 Export FunctorNotations.
 
 Notation "pure[ M ]" := (@pure M _ _)
-  (at level 9, format "pure[ M ]").
+  (at level 0, format "pure[ M ]").
 Notation "pure[ M N ]" := (@pure (fun X => M (N X)) _ _)
-  (at level 9, format "pure[ M  N ]").
+  (at level 0, format "pure[ M  N ]").
 
 Notation "ap[ M ]" := (@ap M _ _ _)
-  (at level 9, format "ap[ M ]").
+  (at level 0, format "ap[ M ]").
 Notation "ap[ M N ]" := (@ap (fun X => M (N X)) _ _ _)
-  (at level 9, format "ap[ M  N ]").
+  (at level 0, format "ap[ M  N ]").
 Notation "ap[ M N O ]" := (@ap (fun X => M (N (O X))) _ _ _)
-  (at level 9, format "ap[ M  N  O ]").
+  (at level 0, format "ap[ M  N  O ]").
 
 Infix "<*>" := ap (at level 29, left associativity).
 Infix "<*[ M ]>" := (@ap M _ _ _)

Theory/Coq/Functor.v

@@ -32,22 +32,22 @@ Notation "x <&> f" := (fmap f x)
   (at level 29, left associativity, only parsing).
 
 Notation "fmap[ M ]" := (@fmap M _ _ _)
-  (at level 9, format "fmap[ M ]").
+  (at level 0, format "fmap[ M ]").
 Notation "fmap[ M N ]" := (@fmap (λ X, M (N X)) _ _ _)
-  (at level 9, format "fmap[ M  N ]").
+  (at level 0, format "fmap[ M  N ]").
 Notation "fmap[ M N O ]" := (@fmap (λ X, M (N (O X))) _ _ _)
-  (at level 9, format "fmap[ M  N  O ]").
+  (at level 0, format "fmap[ M  N  O ]").
 
 Infix ">$<" := contramap (at level 29, left associativity, only parsing).
 Notation "x >&< f" :=
   (contramap f x) (at level 29, left associativity, only parsing).
 
 Notation "contramap[ M ]" := (@contramap M _ _ _)
-  (at level 9, format "contramap[ M ]").
+  (at level 0, format "contramap[ M ]").
 Notation "contramap[ M N ]" := (@contramap (λ X, M (N X)) _ _ _)
-  (at level 9, format "contramap[ M  N ]").
+  (at level 0, format "contramap[ M  N ]").
 Notation "contramap[ M N O ]" := (@contramap (λ X, M (N (O X))) _ _ _)
-  (at level 9, format "contramap[ M  N  O ]").
+  (at level 0, format "contramap[ M  N  O ]").
 
 End FunctorNotations.
 

Theory/Functor.v

@@ -57,9 +57,9 @@ Notation "x <&> f" := (fmap f x)
   (at level 29, left associativity, only parsing) : morphism_scope.
 
 Notation "fobj[ F ]" := (@fobj _ _ F%functor)
-  (at level 9, format "fobj[ F ]") : object_scope.
+  (at level 0, format "fobj[ F ]") : object_scope.
 Notation "fmap[ F ]" := (@fmap _ _ F%functor _ _)
-  (at level 9, format "fmap[ F ]") : morphism_scope.
+  (at level 0, format "fmap[ F ]") : morphism_scope.
 
 #[export] Hint Rewrite @fmap_id : categories.
 
@@ -168,7 +168,7 @@ Program Definition Id {C : Category} : C ⟶ C := {|
 
 Arguments Id {C} /.
 
-Notation "Id[ C ]" := (@Id C) (at level 9, format "Id[ C ]") : functor_scope.
+Notation "Id[ C ]" := (@Id C) (at level 0, format "Id[ C ]") : functor_scope.
 
 Program Definition Compose {C D E : Category}
         (F : D ⟶ E) (G : C ⟶ D) : C ⟶ E := {|