From 90844bf411c7cddcd92d48c0b020e5775ace0849 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Wed, 6 Apr 2011 07:22:14 +0000 Subject: [PATCH] add Notations.v --- src/Adjoints_ch9.v | 2 +- src/Algebras_ch4.v | 2 +- src/BinoidalCategories.v | 2 +- src/Categories_ch1_3.v | 2 +- src/CoEqualizers_ch3_4.v | 2 +- src/Coherence_ch7_8.v | 2 +- src/Enrichment_ch2_8.v | 2 +- src/EpicMonic_ch2_1.v | 2 +- src/Equalizers_ch3_3.v | 2 +- src/EquivalentCategories_ch7_8.v | 2 +- src/FreydCategories.v | 2 +- src/FunctorCategories_ch7_7.v | 2 +- src/Functors_ch1_4.v | 2 +- src/InitialTerminal_ch2_2.v | 2 +- src/Isomorphisms_ch1_5.v | 2 +- src/Main.v | 2 +- src/MonoidalCategories_ch7_8.v | 2 +- src/NaturalIsomorphisms_ch7_5.v | 2 +- src/NaturalTransformations_ch7_4.v | 2 +- src/Notations.v | 93 ++++++++++++++++++++++++++++++++++++ src/OppositeCategories_ch1_6_2.v | 2 +- src/PreMonoidalCategories.v | 2 +- src/PreMonoidalCenter.v | 2 +- src/ProductCategories_ch1_6_1.v | 2 +- src/RepresentableStructure_ch7_2.v | 2 +- src/SectionRetract_ch2_4.v | 2 +- src/SliceCategories_ch1_6_4.v | 2 +- src/Subcategories_ch7_1.v | 2 +- 28 files changed, 120 insertions(+), 27 deletions(-) create mode 100644 src/Notations.v diff --git a/src/Adjoints_ch9.v b/src/Adjoints_ch9.v index 8d947b7..b4361ef 100644 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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. -- 1.7.10.4