add Notations.v

diff --git a/src/Adjoints_ch9.v b/src/Adjoints_ch9.v
index 8d947b7..b4361ef 100644 (file)
--- a/src/Adjoints_ch9.v
+++ b/src/Adjoints_ch9.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Algebras_ch4.v b/src/Algebras_ch4.v
index 24e94bd..c18634d 100644 (file)
--- a/src/Algebras_ch4.v
+++ b/src/Algebras_ch4.v
@@ -6,7 +6,7 @@
 (******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 
 (* very handy *)
 (*

diff --git a/src/BinoidalCategories.v b/src/BinoidalCategories.v
index dddf786..774e8eb 100644 (file)
--- a/src/BinoidalCategories.v
+++ b/src/BinoidalCategories.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Categories_ch1_3.v b/src/Categories_ch1_3.v
index f5786ee..dec78a0 100644 (file)
--- a/src/Categories_ch1_3.v
+++ b/src/Categories_ch1_3.v
@@ -3,7 +3,7 @@
 (******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 
 (* definition 1.1 *)
 Class Category

diff --git a/src/CoEqualizers_ch3_4.v b/src/CoEqualizers_ch3_4.v
index c60a9b6..4ed128e 100644 (file)
--- a/src/CoEqualizers_ch3_4.v
+++ b/src/CoEqualizers_ch3_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 
 (******************************************************************************)
 (* Chapter 3.4: CoEqualizers                                                  *)

diff --git a/src/Coherence_ch7_8.v b/src/Coherence_ch7_8.v
index 2d5f689..20d5920 100644 (file)
--- a/src/Coherence_ch7_8.v
+++ b/src/Coherence_ch7_8.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
index 2fe7d58..a3f4c3e 100644 (file)
--- a/src/Enrichment_ch2_8.v
+++ b/src/Enrichment_ch2_8.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/EpicMonic_ch2_1.v b/src/EpicMonic_ch2_1.v
index 80d95b8..8dc5712 100644 (file)
--- a/src/EpicMonic_ch2_1.v
+++ b/src/EpicMonic_ch2_1.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Equalizers_ch3_3.v b/src/Equalizers_ch3_3.v
index 20b9442..9695d43 100644 (file)
--- a/src/Equalizers_ch3_3.v
+++ b/src/Equalizers_ch3_3.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 
 (******************************************************************************)
 (* Chapter 3.3: Equalizers                                                    *)

diff --git a/src/EquivalentCategories_ch7_8.v b/src/EquivalentCategories_ch7_8.v
index db7f76c..88b71f2 100644 (file)
--- a/src/EquivalentCategories_ch7_8.v
+++ b/src/EquivalentCategories_ch7_8.v
@@ -3,7 +3,7 @@
 (*******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/FreydCategories.v b/src/FreydCategories.v
index 5f0e1c8..b0024fc 100644 (file)
--- a/src/FreydCategories.v
+++ b/src/FreydCategories.v
@@ -3,7 +3,7 @@
 (*******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/FunctorCategories_ch7_7.v b/src/FunctorCategories_ch7_7.v
index 1ed968c..16e5eee 100644 (file)
--- a/src/FunctorCategories_ch7_7.v
+++ b/src/FunctorCategories_ch7_7.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
index ee644ae..12e4489 100644 (file)
--- a/src/Functors_ch1_4.v
+++ b/src/Functors_ch1_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 
 (******************************************************************************)

diff --git a/src/InitialTerminal_ch2_2.v b/src/InitialTerminal_ch2_2.v
index c76208e..864fcab 100644 (file)
--- a/src/InitialTerminal_ch2_2.v
+++ b/src/InitialTerminal_ch2_2.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Isomorphisms_ch1_5.v b/src/Isomorphisms_ch1_5.v
index 372ad43..8241ead 100644 (file)
--- a/src/Isomorphisms_ch1_5.v
+++ b/src/Isomorphisms_ch1_5.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 

diff --git a/src/Main.v b/src/Main.v
index 2a054b7..65ba9c5 100644 (file)
--- a/src/Main.v
+++ b/src/Main.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 8355319..be27f89 100644 (file)
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
index 680e743..c62ba15 100644 (file)
--- a/src/NaturalIsomorphisms_ch7_5.v
+++ b/src/NaturalIsomorphisms_ch7_5.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/NaturalTransformations_ch7_4.v b/src/NaturalTransformations_ch7_4.v
index 0fb6c41..3eee526 100644 (file)
--- a/src/NaturalTransformations_ch7_4.v
+++ b/src/NaturalTransformations_ch7_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Notations.v b/src/Notations.v
new file mode 100644 (file)
index 0000000..3ea525b
--- /dev/null
+++ b/src/Notations.v
@@ -0,0 +1,93 @@
+(*********************************************************************************************************************************)
+(* Notations: miscellaneous notations                                                                                             *)
+(*********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Export Coq.Unicode.Utf8.
+Export Coq.Classes.RelationClasses.
+Export Coq.Classes.Morphisms.
+Export Coq.Setoids.Setoid.
+
+Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
+Generalizable All Variables.
+
+Reserved Notation "a  ~=>  b"                   (at level 70, right associativity).
+Reserved Notation "H ===> C"                    (at level 100).
+Reserved Notation "f >>=>> g"                   (at level 45).
+Reserved Notation "a ~~{ C }~~> b"              (at level 100).
+Reserved Notation "f <--> g"                    (at level 20).
+Reserved Notation "! f"                         (at level 2).
+Reserved Notation "? f"                         (at level 2).
+Reserved Notation "# f"                         (at level 2).
+Reserved Notation "f '⁻¹'"                      (at level 1).
+Reserved Notation "a ≅ b"                       (at level 70, right associativity).
+Reserved Notation "C 'ᵒᴾ'"                      (at level 1).
+Reserved Notation "F \ a"                       (at level 20).
+Reserved Notation "f >>> g"                     (at level 45).
+Reserved Notation "a ~~ b"                      (at level 54).
+Reserved Notation "a ~> b"                      (at level 70, right associativity).
+Reserved Notation "a ≃ b"                       (at level 70, right associativity).
+Reserved Notation "a ≃≃ b"                      (at level 70, right associativity).
+Reserved Notation "a ~~> b"                     (at level 70, right associativity).
+Reserved Notation "F  ~~~> G"                   (at level 70, right associativity).
+Reserved Notation "F <~~~> G"                   (at level 70, right associativity).
+Reserved Notation "a ⊗ b"                       (at level 40).
+Reserved Notation "a ⊗⊗ b"                      (at level 40).
+Reserved Notation "a ⊕  b"                      (at level 40).
+Reserved Notation "a ⊕⊕ b"                      (at level 40).
+Reserved Notation "f ⋉ A"                       (at level 40).
+Reserved Notation "A ⋊ f"                       (at level 40).
+Reserved Notation "- ⋉ A"                       (at level 40).
+Reserved Notation "A ⋊ -"                       (at level 40).
+Reserved Notation "a *** b"                     (at level 40).
+Reserved Notation "a ---> b"                    (at level 11, right associativity).
+Reserved Notation "a <- b"                      (at level 100, only parsing).
+Reserved Notation "a :: b"                      (at level 60, right associativity).
+Reserved Notation "a ++ b"                      (at level 60, right associativity).
+Reserved Notation "f ○ g"                       (at level 100).
+Reserved Notation "f >>>> g"                    (at level 45).
+Reserved Notation "f **** g"                    (at level 40).
+Reserved Notation "C × D"                       (at level 40).
+Reserved Notation "C ×× D"                      (at level 45).
+Reserved Notation "C ⁽ºᑭ⁾"                      (at level 1).
+
+Reserved Notation "F -| G"                      (at level 75).
+Reserved Notation "'ε'".
+Reserved Notation "'η'".
+
+Close Scope nat_scope.  (* so I can redefine '1' *)
+
+Delimit Scope arrow_scope   with arrow.
+Delimit Scope biarrow_scope with biarrow.
+Delimit Scope garrow_scope  with garrow.
+
+Notation "f ○ g"    := (fun x => f(g(x))).
+Notation "a && b"   := (if a then b else false).
+Notation "a || b"   := (if a then true else b).
+
+Notation "∀ x y z u q , P" := (forall x y z u q , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
+  : type_scope.
+Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
+  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,
+    right associativity)
+  : type_scope.

diff --git a/src/OppositeCategories_ch1_6_2.v b/src/OppositeCategories_ch1_6_2.v
index 516334f..ef9fe34 100644 (file)
--- a/src/OppositeCategories_ch1_6_2.v
+++ b/src/OppositeCategories_ch1_6_2.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v
index fdda1a5..6d88657 100644 (file)
--- a/src/PreMonoidalCategories.v
+++ b/src/PreMonoidalCategories.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/PreMonoidalCenter.v b/src/PreMonoidalCenter.v
index 576265d..deb183d 100644 (file)
--- a/src/PreMonoidalCenter.v
+++ b/src/PreMonoidalCenter.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/ProductCategories_ch1_6_1.v b/src/ProductCategories_ch1_6_1.v
index 29d73d4..8373b37 100644 (file)
--- a/src/ProductCategories_ch1_6_1.v
+++ b/src/ProductCategories_ch1_6_1.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
index 2cfe5eb..b928de9 100644 (file)
--- a/src/RepresentableStructure_ch7_2.v
+++ b/src/RepresentableStructure_ch7_2.v
@@ -3,7 +3,7 @@
 (*******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v
index 17ab24a..3053462 100644 (file)
--- a/src/SectionRetract_ch2_4.v
+++ b/src/SectionRetract_ch2_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/SliceCategories_ch1_6_4.v b/src/SliceCategories_ch1_6_4.v
index a9d63df..dba8b1a 100644 (file)
--- a/src/SliceCategories_ch1_6_4.v
+++ b/src/SliceCategories_ch1_6_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index b8412f2..f00a295 100644 (file)
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -3,7 +3,7 @@
 (****************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.