From 5d1c20b74c2d5db1c2ecae97ad1d81f558fdbdba Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 10:05:09 +0200 Subject: [PATCH 01/33] expanding naming conventions --- CODINGSTYLE.md | 76 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 55 insertions(+), 21 deletions(-) diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index e9153c0829..16ee8ee95b 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -247,26 +247,55 @@ the `agda-unimath` library: ## Naming conventions -One of the key strategies to make our library easy to navigate is our naming -convention. We strive for a direct correspondence between a construction's name -and its type. Take, for instance, the proof that the successor function on -integers is an equivalence. It has the type `is-equiv succ-ℤ`, so we name it -`is-equiv-succ-ℤ`. Note how we prefer lowercase and use hyphens to separate -words. - -We also reflect the type of hypotheses used in the construction within the name. -However, the crux of a name primarily describes the type of the constructed -term; descriptions of the hypotheses follow this. For instance, -`is-equiv-is-contr-map` is a function of type `is-contr-map f → is-equiv f`, -where `f` is a given function. Notice how the term `is-equiv-is-contr-map H` -places the descriptor `is-contr-map` right next to the variable `H` it refers -to. - -While abbreviations might seem like a good way to shorten names, we use them -sparingly. They might save a couple of keystrokes for the author, but in the -grand scheme of things, they will likely compromise readability and -maintainability, especially for newcomers and maintainers. We aim for clarity, -not brevity. +A good naming convention is essential for being able to navigate and maintain +the library, and for being able to make progress with your formalization +project. Good names provide coincise descriptions of an entry's purpose, and +help making the code in the library readable. + +The library contains, for example, an entry `is-iso-hom-Ring` for the predicate +that a ring homomorphism is an isomorphsim. The most significant aspect of this +predicate is the assertion that something is an isomorphism. Furthermore, we +make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is +therefore a logical name for the predicate that a ring homomorphism is an +isomorphism. + +In our naming scheme we strive for a direct correspondence between a +constructions's name and its type. Take, for example, the proof that the +successor function on integers is an equivalence. It has the type +`is-equiv succ-ℤ`, so we name it `is-equiv-succ-ℤ`. + +We may also reflect the type of hypotheses used in the construction within the +name. If we wish to do so, we name the hypotheses after we have named the type +of the construction. For instance, `is-equiv-is-contr-map` is a function of type +`is-contr-map f → is-equiv f`, where `f` is a given function. Notice how the +term `is-equiv-is-contr-map H` places the descriptor `is-contr-map` right next +to the variable `H` it refers to. Another advantage is that the name says +immediately what it constructs. + +In general, our naming scheme follows the following pattern: + +```text + [name]-[type]-[hypotheses]-[Important-Concept] +``` + +In this naming scheme all parts are optional, but the order of the different +parts of the name must be respected. + +We saw, for example, that the prediate `is-iso-hom-Ring` has the part `Ring` +capitalized. This signifies that the predicate is about rings. This name follows +the scheme `[name]-[hypotheses]-[Important-Concept]`. Note that there is also +the entry `is-iso-prop-hom-Ring`. This is a predicate that returns for each ring +homomorphism the _proposition_ that it is an isomorphism, and therefore it +follows the scheme `[name]-[type]-[hypotheses]-[Important-Concept]`. Now we can +guess what a construction named `hom-iso-Ring` should be about: It should be a +construction that constructs the underlying homomorphism of an isomorphisms of +rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. + +We should also mention that, while abbreviations might seem like a good way to +shorten names, we use them sparingly. They might save a couple of keystrokes for +the author, but in the grand scheme of things, they will likely compromise +readability and maintainability, especially for newcomers and maintainers. We +aim for clarity, not brevity. Here is a list of our naming conventions: @@ -276,7 +305,8 @@ Here is a list of our naming conventions: - We use US English spelling of words in names. -- Important concepts can be capitalized. Usually, these are categories like +- When an entry is predominantly about objects of an important concept, the + names of these concepts can be capitalized. Usually, these are categories like `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, `Preorder`, `Poset`, `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, and so on. @@ -303,6 +333,10 @@ Here is a list of our naming conventions: [full width equals sign](https://codepoints.net/U+ff1d) for the identity type, as the standard equals sign is a reserved symbol in Agda. +If you are unsure about what to name your entry, ask us on the Univalent Agda +discord server. One of the most commonly asked questions is what to name a +certain thing. + ## Formatting: Indentation, line breaks, and parentheses Code formatting is like punctuation in a novel - it helps readers make sense of From 18e63c42586214884ec352eb54ae81220d6b4ed3 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 10:14:14 +0200 Subject: [PATCH 02/33] separate file for naming conventions --- CODINGSTYLE.md | 115 ---------------------------- Makefile | 1 + scripts/generate_main_index_file.py | 3 +- website/js/custom.js | 1 + 4 files changed, 4 insertions(+), 116 deletions(-) diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index 16ee8ee95b..3eda7c8c4d 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -245,98 +245,6 @@ the `agda-unimath` library: at the moment. All variables are declared either as parameters of an anonymous module or in the type specification of a construction. -## Naming conventions - -A good naming convention is essential for being able to navigate and maintain -the library, and for being able to make progress with your formalization -project. Good names provide coincise descriptions of an entry's purpose, and -help making the code in the library readable. - -The library contains, for example, an entry `is-iso-hom-Ring` for the predicate -that a ring homomorphism is an isomorphsim. The most significant aspect of this -predicate is the assertion that something is an isomorphism. Furthermore, we -make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is -therefore a logical name for the predicate that a ring homomorphism is an -isomorphism. - -In our naming scheme we strive for a direct correspondence between a -constructions's name and its type. Take, for example, the proof that the -successor function on integers is an equivalence. It has the type -`is-equiv succ-ℤ`, so we name it `is-equiv-succ-ℤ`. - -We may also reflect the type of hypotheses used in the construction within the -name. If we wish to do so, we name the hypotheses after we have named the type -of the construction. For instance, `is-equiv-is-contr-map` is a function of type -`is-contr-map f → is-equiv f`, where `f` is a given function. Notice how the -term `is-equiv-is-contr-map H` places the descriptor `is-contr-map` right next -to the variable `H` it refers to. Another advantage is that the name says -immediately what it constructs. - -In general, our naming scheme follows the following pattern: - -```text - [name]-[type]-[hypotheses]-[Important-Concept] -``` - -In this naming scheme all parts are optional, but the order of the different -parts of the name must be respected. - -We saw, for example, that the prediate `is-iso-hom-Ring` has the part `Ring` -capitalized. This signifies that the predicate is about rings. This name follows -the scheme `[name]-[hypotheses]-[Important-Concept]`. Note that there is also -the entry `is-iso-prop-hom-Ring`. This is a predicate that returns for each ring -homomorphism the _proposition_ that it is an isomorphism, and therefore it -follows the scheme `[name]-[type]-[hypotheses]-[Important-Concept]`. Now we can -guess what a construction named `hom-iso-Ring` should be about: It should be a -construction that constructs the underlying homomorphism of an isomorphisms of -rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. - -We should also mention that, while abbreviations might seem like a good way to -shorten names, we use them sparingly. They might save a couple of keystrokes for -the author, but in the grand scheme of things, they will likely compromise -readability and maintainability, especially for newcomers and maintainers. We -aim for clarity, not brevity. - -Here is a list of our naming conventions: - -- Names are unique; we steer clear of namespace overloading. - -- Names should accurately convey the concept of its construction. - -- We use US English spelling of words in names. - -- When an entry is predominantly about objects of an important concept, the - names of these concepts can be capitalized. Usually, these are categories like - `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, `Preorder`, `Poset`, - `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, and so on. - -- As a general rule of thumb, names should start out with an all lowercase - portion with words separated by hyphens, and may have a capitalized portion at - the end that describes which larger mathematical framework the definition - takes place in -- for instance, if it is constructed internally to a certain - subuniverse or category of mathematical objects. - -- The start of a name describes the object that is being constructed. For some - theorems, the latter part of a name describes the hypotheses. - -- Names never reference variables. - -- We use Unicode symbols sparingly and only when they align with established - mathematical practice. - -- Just as we do with abbreviations, we use special symbols sparingly in names. - -- If a symbol is not available, we describe the concept concisely in words. - -- We prioritize the readability of the code and avoid subtly different - variations of the same symbol. An important exception is the use of the - [full width equals sign](https://codepoints.net/U+ff1d) for the identity type, - as the standard equals sign is a reserved symbol in Agda. - -If you are unsure about what to name your entry, ask us on the Univalent Agda -discord server. One of the most commonly asked questions is what to name a -certain thing. - ## Formatting: Indentation, line breaks, and parentheses Code formatting is like punctuation in a novel - it helps readers make sense of @@ -439,14 +347,6 @@ the story. Here's how we handle indentation and line breaks in the ## Coding practices we tend to avoid -- Using Unicode characters in names is entirely permissible, but we recommend - restraint to maintain readability. Just a few well-placed symbols can often - express a lot. - -- To enhance conceptual clarity, we suggest names of constructions avoid - referring to variable names. This makes code more understandable, even at a - glance, and easier to work with in subsequent code. - - We encourage limiting the depth increase of indentation levels to two spaces. This practice tends to keep our code reader-friendly, especially on smaller screens, by keeping more code on the left-hand side of the screen. In @@ -467,21 +367,6 @@ the story. Here's how we handle indentation and line breaks in the However, when the identity type isn't as critical, feel free to use record types as they can be convenient. -- Using the projection functions `pr1` and `pr2`, particularly their - compositions, can lead to short code, but we recommend to avoid doing so. When - constructions contain a lot of projections throughout their definition, the - projections reveal little of what is going on in that part of the projections. - We therefore prefer naming the projections. When a type of the form `Σ A B` is - given a name, naming its projections too can enhance readability and will - provide more informative responses when jumping to the definition. - Furthermore, it makes it easier to change the definition later on. - -- Lastly, we recommend not naming constructions after infix notation of - operations included in them. Preferring primary prefix notation over infix - notation can help keep our code consistent. For example, it's preferred to use - `commutative-prod` instead of `commutative-×` for denoting the commutativity - of cartesian products. - These guidelines are here to make everyone's coding experience more enjoyable and productive. As always, your contributions to the `agda-unimath` library are valued, and these suggestions are here to help ensure that your code is clear, diff --git a/Makefile b/Makefile index 6d4fab320f..d522aed9d4 100644 --- a/Makefile +++ b/Makefile @@ -25,6 +25,7 @@ METAFILES := \ LICENSE.md \ MIXFIX-OPERATORS.md \ MAINTAINERS.md \ + NAMING.md \ README.md \ STATEMENT-OF-INCLUSION.md \ SUMMARY.md \ diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py index 7eda128484..682f241645 100755 --- a/scripts/generate_main_index_file.py +++ b/scripts/generate_main_index_file.py @@ -101,7 +101,8 @@ def generate_index(root, header): - [Structuring your file](FILE-CONVENTIONS.md) - [File template](TEMPLATE.lagda.md) - [The library coding style](CODINGSTYLE.md) - - [Guidelines for mixfix operators](MIXFIX-OPERATORS.md) + - [Naming conventions](NAMING.md) + - [Mixfix operators](MIXFIX-OPERATORS.md) - [Citing the library](CITE-THIS-LIBRARY.md) - [Library contents](SUMMARY.md) - [Art](ART.md) diff --git a/website/js/custom.js b/website/js/custom.js index 53ac7ab21c..2dd014fe43 100644 --- a/website/js/custom.js +++ b/website/js/custom.js @@ -16,6 +16,7 @@ if (link) { 'LICENSE.md', 'MAINTAINERS.md', 'MIXFIX-OPERATORS.md', + 'NAMING.md', 'README.md', 'STATEMENT-OF-INCLUSION.md', 'SUMMARY.md', From efd8af38f937f09252cbd4417856ad409662974e Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 10:14:21 +0200 Subject: [PATCH 03/33] separate file for naming conventions --- NAMING.md | 116 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 NAMING.md diff --git a/NAMING.md b/NAMING.md new file mode 100644 index 0000000000..30dd86660d --- /dev/null +++ b/NAMING.md @@ -0,0 +1,116 @@ +# Naming conventions + +A good naming convention is essential for being able to navigate and maintain +the library, and for being able to make progress with your formalization +project. Good names provide coincise descriptions of an entry's purpose, and +help making the code in the library readable. + +The library contains, for example, an entry `is-iso-hom-Ring` for the predicate +that a ring homomorphism is an isomorphsim. The most significant aspect of this +predicate is the assertion that something is an isomorphism. Furthermore, we +make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is +therefore a logical name for the predicate that a ring homomorphism is an +isomorphism. + +In our naming scheme we strive for a direct correspondence between a +constructions's name and its type. Take, for example, the proof that the +successor function on integers is an equivalence. It has the type +`is-equiv succ-ℤ`, so we name it `is-equiv-succ-ℤ`. + +We may also reflect the type of hypotheses used in the construction within the +name. If we wish to do so, we name the hypotheses after we have named the type +of the construction. For instance, `is-equiv-is-contr-map` is a function of type +`is-contr-map f → is-equiv f`, where `f` is a given function. Notice how the +term `is-equiv-is-contr-map H` places the descriptor `is-contr-map` right next +to the variable `H` it refers to. Another advantage is that the name says +immediately what it constructs. + +In general, our naming scheme follows the following pattern: + +```text + [name]-[type]-[hypotheses]-[Important-Concept] +``` + +In this naming scheme all parts are optional, but the order of the different +parts of the name must be respected. + +We saw, for example, that the prediate `is-iso-hom-Ring` has the part `Ring` +capitalized. This signifies that the predicate is about rings. This name follows +the scheme `[name]-[hypotheses]-[Important-Concept]`. Note that there is also +the entry `is-iso-prop-hom-Ring`. This is a predicate that returns for each ring +homomorphism the _proposition_ that it is an isomorphism, and therefore it +follows the scheme `[name]-[type]-[hypotheses]-[Important-Concept]`. Now we can +guess what a construction named `hom-iso-Ring` should be about: It should be a +construction that constructs the underlying homomorphism of an isomorphisms of +rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. + +We should also mention that, while abbreviations might seem like a good way to +shorten names, we use them sparingly. They might save a couple of keystrokes for +the author, but in the grand scheme of things, they will likely compromise +readability and maintainability, especially for newcomers and maintainers. We +aim for clarity, not brevity. + +## Overview of our naming conventions + +- Names are unique; we steer clear of namespace overloading. + +- Names should accurately convey the concept of its construction. + +- We use US English spelling of words in names. + +- When an entry is predominantly about objects of an important concept, the + names of these concepts can be capitalized. Usually, these are categories like + `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, `Preorder`, `Poset`, + `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, and so on. + +- As a general rule of thumb, names should start out with an all lowercase + portion with words separated by hyphens, and may have a capitalized portion at + the end that describes which larger mathematical framework the definition + takes place in -- for instance, if it is constructed internally to a certain + subuniverse or category of mathematical objects. + +- The start of a name describes the object that is being constructed. For some + theorems, the latter part of a name describes the hypotheses. + +- We use Unicode symbols sparingly and only when they align with established + mathematical practice. + +- Just as we do with abbreviations, we use special symbols sparingly in names. + +- If a symbol is not available, we describe the concept concisely in words. + +- We prioritize the readability of the code and avoid subtly different + variations of the same symbol. An important exception is the use of the + [full width equals sign](https://codepoints.net/U+ff1d) for the identity type, + as the standard equals sign is a reserved symbol in Agda. + +If you are unsure about what to name your entry, ask us on the Univalent Agda +discord server. One of the most commonly asked questions is what to name a +certain thing. + +## Naming conventions we try to avoid + +- Using Unicode characters in names is entirely permissible, but we recommend + restraint to maintain readability. Just a few well-placed symbols can often + express a lot. + +- To enhance conceptual clarity, we suggest names of constructions avoid + referring to variable names. This makes code more understandable, even at a + glance, and easier to work with in subsequent code. + +- Using the projection functions `pr1` and `pr2`, particularly their + compositions, can lead to short code, but we recommend to avoid doing so. When + constructions contain a lot of projections throughout their definition, the + projections reveal little of what is going on in that part of the projections. + We therefore prefer naming the projections. When a type of the form `Σ A B` is + given a name, naming its projections too can enhance readability and will + provide more informative responses when jumping to the definition. + Furthermore, it makes it easier to change the definition later on. + +- Lastly, we recommend not naming constructions after infix notation of + operations included in them. Preferring primary prefix notation over infix + notation can help keep our code consistent. For example, it's preferred to use + `commutative-prod` instead of `commutative-×` for denoting the commutativity + of cartesian products. + +- Names never reference variables. \ No newline at end of file From d8a9cd6ca8d1b52e5f55f7a17eb6457f99e8528e Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 10:18:46 +0200 Subject: [PATCH 04/33] make pre-commit --- NAMING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/NAMING.md b/NAMING.md index 30dd86660d..2d1fb2dd17 100644 --- a/NAMING.md +++ b/NAMING.md @@ -113,4 +113,4 @@ certain thing. `commutative-prod` instead of `commutative-×` for denoting the commutativity of cartesian products. -- Names never reference variables. \ No newline at end of file +- Names never reference variables. From 0b4e67b86481af94c9994e6828dbdf308d75b2cf Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 22:37:18 +0200 Subject: [PATCH 05/33] explaining the naming of underlying objects --- NAMING.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/NAMING.md b/NAMING.md index 2d1fb2dd17..d4312f4e75 100644 --- a/NAMING.md +++ b/NAMING.md @@ -44,6 +44,8 @@ guess what a construction named `hom-iso-Ring` should be about: It should be a construction that constructs the underlying homomorphism of an isomorphisms of rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. +There is also a common class of cases where we don't use the `[name]` part in the name of an entry: underlying objects. For example, the underlying set of a group is called `set-Group`, which uses the pattern `[type]-[Important-Concept]`. The construction of the underlying set of a group returns for each group a set, which is an element of type `Set`. Similarly, we have `type-Group]`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on. Another instance where this happens is in `hom-iso-Group`, which is the construction that returns the underlying group homomorphism of an isomorphism of group. The fact that a group isomorphism is an isomorphsim is called `is-iso-iso-Group`, which also uses the pattern `[type]-[Important-Concept]`. One could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the underlying group homomorphism of the isomorphism is an isomorphism. However, this name does not fit our patterns in any way, and the addition of `hom` to the name adds no extra useful information. This situation is common in instances where we omit the `[name]` part of a name. For instance `[is-category-Category` and `is-ideal-ideal-Ring` follow the patterns `[type]-[Important-Concept]` and `[type]-[hypotheses]-[Important-Concept]`. + We should also mention that, while abbreviations might seem like a good way to shorten names, we use them sparingly. They might save a couple of keystrokes for the author, but in the grand scheme of things, they will likely compromise From 1f470b1b23dc289a2bee02644abcad9284b480b7 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 22:37:41 +0200 Subject: [PATCH 06/33] make pre-commit --- NAMING.md | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/NAMING.md b/NAMING.md index d4312f4e75..5952111d4b 100644 --- a/NAMING.md +++ b/NAMING.md @@ -44,7 +44,23 @@ guess what a construction named `hom-iso-Ring` should be about: It should be a construction that constructs the underlying homomorphism of an isomorphisms of rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. -There is also a common class of cases where we don't use the `[name]` part in the name of an entry: underlying objects. For example, the underlying set of a group is called `set-Group`, which uses the pattern `[type]-[Important-Concept]`. The construction of the underlying set of a group returns for each group a set, which is an element of type `Set`. Similarly, we have `type-Group]`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on. Another instance where this happens is in `hom-iso-Group`, which is the construction that returns the underlying group homomorphism of an isomorphism of group. The fact that a group isomorphism is an isomorphsim is called `is-iso-iso-Group`, which also uses the pattern `[type]-[Important-Concept]`. One could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the underlying group homomorphism of the isomorphism is an isomorphism. However, this name does not fit our patterns in any way, and the addition of `hom` to the name adds no extra useful information. This situation is common in instances where we omit the `[name]` part of a name. For instance `[is-category-Category` and `is-ideal-ideal-Ring` follow the patterns `[type]-[Important-Concept]` and `[type]-[hypotheses]-[Important-Concept]`. +There is also a common class of cases where we don't use the `[name]` part in +the name of an entry: underlying objects. For example, the underlying set of a +group is called `set-Group`, which uses the pattern +`[type]-[Important-Concept]`. The construction of the underlying set of a group +returns for each group a set, which is an element of type `Set`. Similarly, we +have `type-Group]`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on. +Another instance where this happens is in `hom-iso-Group`, which is the +construction that returns the underlying group homomorphism of an isomorphism of +group. The fact that a group isomorphism is an isomorphsim is called +`is-iso-iso-Group`, which also uses the pattern `[type]-[Important-Concept]`. +One could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the +underlying group homomorphism of the isomorphism is an isomorphism. However, +this name does not fit our patterns in any way, and the addition of `hom` to the +name adds no extra useful information. This situation is common in instances +where we omit the `[name]` part of a name. For instance `[is-category-Category` +and `is-ideal-ideal-Ring` follow the patterns `[type]-[Important-Concept]` and +`[type]-[hypotheses]-[Important-Concept]`. We should also mention that, while abbreviations might seem like a good way to shorten names, we use them sparingly. They might save a couple of keystrokes for From 3d521a86889260330da2e2c0c658e7b345d02f16 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 22:45:02 +0200 Subject: [PATCH 07/33] Update NAMING.md Co-authored-by: Fredrik Bakke --- NAMING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/NAMING.md b/NAMING.md index 5952111d4b..f8f803cba9 100644 --- a/NAMING.md +++ b/NAMING.md @@ -13,7 +13,7 @@ therefore a logical name for the predicate that a ring homomorphism is an isomorphism. In our naming scheme we strive for a direct correspondence between a -constructions's name and its type. Take, for example, the proof that the +construction's name and its type. Take, for example, the proof that the successor function on integers is an equivalence. It has the type `is-equiv succ-ℤ`, so we name it `is-equiv-succ-ℤ`. From 92c28a49100ee89db71fb8a2635016664c4087cc Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 22:47:03 +0200 Subject: [PATCH 08/33] fix broken links --- CODINGSTYLE.md => CODING-STYLE.md | 0 HOWTO-INSTALL.md => HOW-TO-INSTALL.md | 6 +++--- Makefile | 6 +++--- NAMING.md => NAMING-CONVENTIONS.md | 0 scripts/generate_main_index_file.py | 6 +++--- website/js/custom.js | 6 +++--- 6 files changed, 12 insertions(+), 12 deletions(-) rename CODINGSTYLE.md => CODING-STYLE.md (100%) rename HOWTO-INSTALL.md => HOW-TO-INSTALL.md (98%) rename NAMING.md => NAMING-CONVENTIONS.md (100%) diff --git a/CODINGSTYLE.md b/CODING-STYLE.md similarity index 100% rename from CODINGSTYLE.md rename to CODING-STYLE.md diff --git a/HOWTO-INSTALL.md b/HOW-TO-INSTALL.md similarity index 98% rename from HOWTO-INSTALL.md rename to HOW-TO-INSTALL.md index a0eb4d04f2..1432fdeb80 100644 --- a/HOWTO-INSTALL.md +++ b/HOW-TO-INSTALL.md @@ -216,8 +216,8 @@ width equals sign `＝`. While you're at it, you can also add the key sequence #### 80-character limit The `agda-unimath` library maintains an 80-character limit on the length of most -lines in the source code (see [CODINGSTYLE](CODINGSTYLE.md#character-limit) for -a list of exceptions). This limit is to improve readability, both in your +lines in the source code (see [CODING-STYLE](CODING-STYLE.md#character-limit) +for a list of exceptions). This limit is to improve readability, both in your programming environment and on our website. To display a vertical ruler marking the 80th column in Emacs, add: @@ -300,7 +300,7 @@ in the library. We welcome and appreciate contributions from the community. If you're interested in contributing to the `agda-unimath` library, you can follow the instructions below to ensure a smooth setup and workflow. Also, please make sure to follow -our [coding style](CODINGSTYLE.md) and +our [coding style](CODING-STYLE.md) and [design principles](DESIGN-PRINCIPLES.md). ### Pre-commit hooks and Python dependencies diff --git a/Makefile b/Makefile index d522aed9d4..62993741c1 100644 --- a/Makefile +++ b/Makefile @@ -14,18 +14,18 @@ TIME ?= time METAFILES := \ ART.md \ CITE-THIS-LIBRARY.md \ - CODINGSTYLE.md \ + CODING-STYLE.md \ CONTRIBUTING.md \ CONTRIBUTORS.md \ FILE-CONVENTIONS.md \ DESIGN-PRINCIPLES.md \ GRANT-ACKNOWLEDGEMENTS.md \ HOME.md \ - HOWTO-INSTALL.md \ + HOW-TO-INSTALL.md \ LICENSE.md \ MIXFIX-OPERATORS.md \ MAINTAINERS.md \ - NAMING.md \ + NAMING-CONVENTIONS.md \ README.md \ STATEMENT-OF-INCLUSION.md \ SUMMARY.md \ diff --git a/NAMING.md b/NAMING-CONVENTIONS.md similarity index 100% rename from NAMING.md rename to NAMING-CONVENTIONS.md diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py index 682f241645..b4519ee51e 100755 --- a/scripts/generate_main_index_file.py +++ b/scripts/generate_main_index_file.py @@ -95,13 +95,13 @@ def generate_index(root, header): - [Projects using Agda-Unimath](USERS.md) - [Grant acknowledgements](GRANT-ACKNOWLEDGEMENTS.md) - [Guides](HOWTO-INSTALL.md) - - [Installing the library](HOWTO-INSTALL.md) + - [Installing the library](HOW-TO-INSTALL.md) - [Design principles](DESIGN-PRINCIPLES.md) - [Contributing to the library](CONTRIBUTING.md) - [Structuring your file](FILE-CONVENTIONS.md) - [File template](TEMPLATE.lagda.md) - - [The library coding style](CODINGSTYLE.md) - - [Naming conventions](NAMING.md) + - [The library coding style](CODING-STYLE.md) + - [Naming conventions](NAMING-CONVENTIONS.md) - [Mixfix operators](MIXFIX-OPERATORS.md) - [Citing the library](CITE-THIS-LIBRARY.md) - [Library contents](SUMMARY.md) diff --git a/website/js/custom.js b/website/js/custom.js index 2dd014fe43..e2e82ea518 100644 --- a/website/js/custom.js +++ b/website/js/custom.js @@ -5,18 +5,18 @@ if (link) { const fileList = [ 'ART.md', 'CITE-THIS-LIBRARY.md', - 'CODINGSTYLE.md', + 'CODING-STYLE.md', 'CONTRIBUTING.md', 'CONTRIBUTORS.md', 'DESIGN-PRINCIPLES.md', 'FILE-CONVENTIONS.md', 'GRANT-ACKNOWLEDGEMENTS.md', 'HOME.md', - 'HOWTO-INSTALL.md', + 'HOW-TO-INSTALL.md', 'LICENSE.md', 'MAINTAINERS.md', 'MIXFIX-OPERATORS.md', - 'NAMING.md', + 'NAMING-CONVENTIONS.md', 'README.md', 'STATEMENT-OF-INCLUSION.md', 'SUMMARY.md', From d9ee159d35ff561a9c202154e2f16006de6be836 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 23:30:13 +0200 Subject: [PATCH 09/33] sectioning --- NAMING-CONVENTIONS.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index f8f803cba9..83161fb2a8 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -3,7 +3,10 @@ A good naming convention is essential for being able to navigate and maintain the library, and for being able to make progress with your formalization project. Good names provide coincise descriptions of an entry's purpose, and -help making the code in the library readable. +help making the code in the library readable. On this page we provide general +guidelines for naming entries that apply anywhere in the library. + +## Examples The library contains, for example, an entry `is-iso-hom-Ring` for the predicate that a ring homomorphism is an isomorphsim. The most significant aspect of this @@ -25,6 +28,8 @@ term `is-equiv-is-contr-map H` places the descriptor `is-contr-map` right next to the variable `H` it refers to. Another advantage is that the name says immediately what it constructs. +## The general scheme + In general, our naming scheme follows the following pattern: ```text @@ -62,6 +67,8 @@ where we omit the `[name]` part of a name. For instance `[is-category-Category` and `is-ideal-ideal-Ring` follow the patterns `[type]-[Important-Concept]` and `[type]-[hypotheses]-[Important-Concept]`. +## Abbreviations, and avoiding them + We should also mention that, while abbreviations might seem like a good way to shorten names, we use them sparingly. They might save a couple of keystrokes for the author, but in the grand scheme of things, they will likely compromise @@ -132,3 +139,11 @@ certain thing. of cartesian products. - Names never reference variables. + +Finally, we should mention that the naming scheme of agda-unimath evolves as +agda grows. Sometimes we find that old namings don't fit our ideas of a good +naming scheme anymore, or we find other ways to improve on the naming. Some +older code in the library might even not be updated yet to fit the current +naming scheme. We should therefore remember that the naming scheme is not set in +stone, and maintaining and improving it is part of the work of maintaining the +agda-unimath library. From e91cf2e025c66943275e57858eb33f5aa8c3d82b Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 23:41:29 +0200 Subject: [PATCH 10/33] adding gregor --- scripts/contributors_data.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/contributors_data.toml b/scripts/contributors_data.toml index 0b3808f2d0..a47e48295d 100644 --- a/scripts/contributors_data.toml +++ b/scripts/contributors_data.toml @@ -233,3 +233,8 @@ github = "andrejbauer" displayName = "Matej Petković" usernames = [ "Matej Petković" ] github = "Petkomat" + +[[contributors]] +displayName = "Gregor Perčič" +usernames = [ "Gregor Perčič" ] +github = "GregorPercic" \ No newline at end of file From 0ab40db98194f651289ef9fd5e8b2514b25030c1 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 21 Sep 2023 23:43:20 +0200 Subject: [PATCH 11/33] make pre-commit --- scripts/contributors_data.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/contributors_data.toml b/scripts/contributors_data.toml index a47e48295d..3f2a878b2a 100644 --- a/scripts/contributors_data.toml +++ b/scripts/contributors_data.toml @@ -237,4 +237,4 @@ github = "Petkomat" [[contributors]] displayName = "Gregor Perčič" usernames = [ "Gregor Perčič" ] -github = "GregorPercic" \ No newline at end of file +github = "GregorPercic" From a44bd4595ad8d9c549d31ea33268a5901e1e9a4b Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 12:46:46 +0200 Subject: [PATCH 12/33] further explaining our naming conventions --- NAMING-CONVENTIONS.md | 125 +++++++++++++++++++++++++++++++----------- 1 file changed, 93 insertions(+), 32 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 83161fb2a8..320abb5428 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -6,6 +6,24 @@ project. Good names provide coincise descriptions of an entry's purpose, and help making the code in the library readable. On this page we provide general guidelines for naming entries that apply anywhere in the library. +We also mention that the naming scheme of agda-unimath evolves as agda grows. +Sometimes we find that old namings don't fit our ideas of a good naming scheme +anymore, or we find other ways to improve on the naming. Some older code in the +library might even not be updated yet to fit the current naming scheme. We +should therefore remember that the naming scheme is not set in stone, and +maintaining and improving it is part of the work of maintaining the agda-unimath +library. + +Finally, we should note that accurately naming entries in a large formalization +project can be very difficult, especially when your formalization enters +unchartered, or little written about territory. Giving good names to your +entries requires a high level of conceptual understanding of your entries. The +naming scheme should help reveal common patterns in names, which hopefully helps +to find predictable namings for entries. On the other hand, we understand that +this is not always possible. If you find yourself not knowing what to name +something, give it your best shot to come up with a name, or reach out to us on +the Univalent Agda discord to ask if we have any suggestions. + ## Examples The library contains, for example, an entry `is-iso-hom-Ring` for the predicate @@ -33,39 +51,90 @@ immediately what it constructs. In general, our naming scheme follows the following pattern: ```text - [name]-[type]-[hypotheses]-[Important-Concept] + [name]-[type]-[hypotheses]-[Namespace] ``` -In this naming scheme all parts are optional, but the order of the different -parts of the name must be respected. +We note that Agda has, as of yet, no namespace mechanism. This means that in +places where we wished to be able to use namespaces, we would append the name of +an entry with the name that we would have given to that namespace. We use this +naming convention for important mathematical concepts, such as groups, rings, +categories, graphs, trees, and so on. Furthermore, we note that in the general +naming scheme above all parts are optional, but the order of the different parts +of the name must be respected. + +### Naming mathematical structures We saw, for example, that the prediate `is-iso-hom-Ring` has the part `Ring` capitalized. This signifies that the predicate is about rings. This name follows -the scheme `[name]-[hypotheses]-[Important-Concept]`. Note that there is also -the entry `is-iso-prop-hom-Ring`. This is a predicate that returns for each ring +the scheme `[name]-[hypotheses]-[Namespace]`. Note that there is also the entry +`is-iso-prop-hom-Ring`. This is a predicate that returns for each ring homomorphism the _proposition_ that it is an isomorphism, and therefore it -follows the scheme `[name]-[type]-[hypotheses]-[Important-Concept]`. Now we can -guess what a construction named `hom-iso-Ring` should be about: It should be a +follows the scheme `[name]-[type]-[hypotheses]-[Namespace]`. Now we can guess +what a construction named `hom-iso-Ring` should be about: It should be a construction that constructs the underlying homomorphism of an isomorphisms of -rings. This name follows the pattern `[type]-[hypotheses]-[Important-Concept]`. +rings. This name follows the pattern `[type]-[hypotheses]-[Namespace]`. -There is also a common class of cases where we don't use the `[name]` part in +There is also a common class of entries where we don't use the `[name]` part in the name of an entry: underlying objects. For example, the underlying set of a -group is called `set-Group`, which uses the pattern -`[type]-[Important-Concept]`. The construction of the underlying set of a group -returns for each group a set, which is an element of type `Set`. Similarly, we -have `type-Group]`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on. -Another instance where this happens is in `hom-iso-Group`, which is the -construction that returns the underlying group homomorphism of an isomorphism of -group. The fact that a group isomorphism is an isomorphsim is called -`is-iso-iso-Group`, which also uses the pattern `[type]-[Important-Concept]`. -One could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the -underlying group homomorphism of the isomorphism is an isomorphism. However, -this name does not fit our patterns in any way, and the addition of `hom` to the -name adds no extra useful information. This situation is common in instances -where we omit the `[name]` part of a name. For instance `[is-category-Category` -and `is-ideal-ideal-Ring` follow the patterns `[type]-[Important-Concept]` and -`[type]-[hypotheses]-[Important-Concept]`. +group is called `set-Group`, which uses the pattern `[type]-[Namespace]`. The +construction of the underlying set of a group returns for each group a set, +which is an element of type `Set`. Similarly, we have `type-Group]`, +`semigroup-Group`, `type-Ring`, `set-Ring`, and so on. Another instance where +this happens is in `hom-iso-Group`, which is the construction that returns the +underlying group homomorphism of an isomorphism of group. The fact that a group +isomorphism is an isomorphsim is called `is-iso-iso-Group`, which also uses the +pattern `[type]-[Namespace]`. One could also consider calling it +`is-iso-hom-iso-Group`, to emphasize that the underlying group homomorphism of +the isomorphism is an isomorphism. However, this name does not fit our patterns +in any way, and the addition of `hom` to the name adds no extra useful +information. This situation is common in instances where we omit the `[name]` +part of a name. For instance `[is-category-Category` and `is-ideal-ideal-Ring` +follow the patterns `[type]-[Namespace]` and `[type]-[hypotheses]-[Namespace]`. + +Another class of entries where the naming scheme needs some explanation, is +where we define a structured object from another structured object. For +instance, the [kernel](group-theory.kernels.md) of a +[group homomorphism](group-theory.homomorphisms-groups.md) is defined to be the +[normal subgroup](group-theory.normal-subgroups.md) `kernel-hom-Group`. This +name follows the scheme +`[name]-[hypotheses]-[Namespace]`. When we want to define the underlying structure of the kernel of a group homomorphism, we follow the scheme `[type]-[hypotheses]-[Namespace]`. For instance, the underlying group of the kernel of a group homomorphism is called `group-kernel-hom-Group`. + +### Naming conventions for mathematical laws + +Often, mathematical laws are recorded by first specifying in full generality +what it means to satisfy that law. For example, the +[unit laws](foundation.unital-binary-operations.md) for a binary operation are +stated as `left-unit-law` and `right-unit-law`. The fact that +[multiplication on the integers](elementary-number-theory.multiplication-integers.md) +satisfies the unit laws is then stated as `left-unit-law-mul-ℤ` and +`right-unit-law-mul-ℤ`. In the general naming scheme, this naming follows the +pattern `[type]-[Namespace]`, because it states the type of which an element is +constructed, and we treat `ℤ` as a namespace. + +For a second example, `interchange-law` states what it means to satisfy the +[interchange law](foundation.interchange-law.md). This interchange law requires +two operations. When we want to prove an interchange law for two specific +operations `mul1` and `mul2`, we name it `interchange-law-mul1-mul2`. We use +this naming scheme, even if the two operations are the same. In fact two +_associative_ operations that satisfy the interchange law will necessarily be +the same. For example, in the [integers](elementary-number-theory.integers.md) +there is an interchange law for addition over addition, which states that +`(a + b) + (c + d) ＝ (a + c) + (b + d)`. This law is called +`interchange-law-add-add-ℤ`. Again, this naming follows the pattern +`[type]-[Namespace]`, because it states the type of which an element is +constructed. + +### Further naming conventions for operations on types + +It is also common that we have to record computation laws for functions. For +instance, +[transport along identifications](foundation.transport-along-identifications.md) +in a family of [loop spaces](synthetic-homotopy-theory.loop-spaces.md) acts by +[conjugation](synthetic-homotopy-theory.conjugation-loops.md). The name for +transport along identifications is `tr` and the name for loop spaces in the +library is `Ω`. Therefore, we record the function that transport computes to as +`tr-Ω` and we record the [homotopy](foundation.homotopies.md) that transport is +pointwise equal to `tr-Ω` as `compute-tr-Ω`. ## Abbreviations, and avoiding them @@ -139,11 +208,3 @@ certain thing. of cartesian products. - Names never reference variables. - -Finally, we should mention that the naming scheme of agda-unimath evolves as -agda grows. Sometimes we find that old namings don't fit our ideas of a good -naming scheme anymore, or we find other ways to improve on the naming. Some -older code in the library might even not be updated yet to fit the current -naming scheme. We should therefore remember that the naming scheme is not set in -stone, and maintaining and improving it is part of the work of maintaining the -agda-unimath library. From 2b17fa6d5c8fb016fdbbf6ab9d58ab784f842fb2 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 12:48:04 +0200 Subject: [PATCH 13/33] make pre-commit --- NAMING-CONVENTIONS.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 320abb5428..50133aa484 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -96,8 +96,10 @@ where we define a structured object from another structured object. For instance, the [kernel](group-theory.kernels.md) of a [group homomorphism](group-theory.homomorphisms-groups.md) is defined to be the [normal subgroup](group-theory.normal-subgroups.md) `kernel-hom-Group`. This -name follows the scheme -`[name]-[hypotheses]-[Namespace]`. When we want to define the underlying structure of the kernel of a group homomorphism, we follow the scheme `[type]-[hypotheses]-[Namespace]`. For instance, the underlying group of the kernel of a group homomorphism is called `group-kernel-hom-Group`. +name follows the scheme `[name]-[hypotheses]-[Namespace]`. When we want to +define the underlying structure of the kernel of a group homomorphism, we follow +the scheme `[type]-[hypotheses]-[Namespace]`. For instance, the underlying group +of the kernel of a group homomorphism is called `group-kernel-hom-Group`. ### Naming conventions for mathematical laws From 1d30aa6fc028853d839c561b58bd8227f84e7fa4 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 12:57:45 +0200 Subject: [PATCH 14/33] further comments --- NAMING-CONVENTIONS.md | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 50133aa484..ebf82fd897 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -88,7 +88,7 @@ pattern `[type]-[Namespace]`. One could also consider calling it the isomorphism is an isomorphism. However, this name does not fit our patterns in any way, and the addition of `hom` to the name adds no extra useful information. This situation is common in instances where we omit the `[name]` -part of a name. For instance `[is-category-Category` and `is-ideal-ideal-Ring` +part of a name. For instance `is-category-Category` and `is-ideal-ideal-Ring` follow the patterns `[type]-[Namespace]` and `[type]-[hypotheses]-[Namespace]`. Another class of entries where the naming scheme needs some explanation, is @@ -138,14 +138,6 @@ library is `Ω`. Therefore, we record the function that transport computes to as `tr-Ω` and we record the [homotopy](foundation.homotopies.md) that transport is pointwise equal to `tr-Ω` as `compute-tr-Ω`. -## Abbreviations, and avoiding them - -We should also mention that, while abbreviations might seem like a good way to -shorten names, we use them sparingly. They might save a couple of keystrokes for -the author, but in the grand scheme of things, they will likely compromise -readability and maintainability, especially for newcomers and maintainers. We -aim for clarity, not brevity. - ## Overview of our naming conventions - Names are unique; we steer clear of namespace overloading. @@ -186,9 +178,20 @@ certain thing. ## Naming conventions we try to avoid -- Using Unicode characters in names is entirely permissible, but we recommend - restraint to maintain readability. Just a few well-placed symbols can often - express a lot. +- Abbreviations might seem like a good way to shorten names, but we use them + sparingly. They might save a couple of keystrokes for the author, but in the + grand scheme of things, they will likely compromise readability and + maintainability, especially for newcomers and maintainers. We aim for clarity, + not brevity. + +- Using Unicode characters in names is permissible, but we recommend restraint + to maintain readability. Just a few well-placed symbols can often express a + lot. Often, when we introduce mixfix operators, we also introduce full names + for them. We then use the full names for these operators in the naming scheme, + and omit the symbolic notation for anything but the operation itself. For + example, the commutativity of cartesian products is called `commutative-prod` + and not `commutative-×`, and the unit of a modality is called `unit-modality` + and not `unit-○`. - To enhance conceptual clarity, we suggest names of constructions avoid referring to variable names. This makes code more understandable, even at a From c922269fe978405c0716fb640fc13cdf52ed06b1 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 13:25:23 +0200 Subject: [PATCH 15/33] revised introduction --- NAMING-CONVENTIONS.md | 39 +++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 18 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index ebf82fd897..c8a1dbaa86 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -2,27 +2,30 @@ A good naming convention is essential for being able to navigate and maintain the library, and for being able to make progress with your formalization -project. Good names provide coincise descriptions of an entry's purpose, and -help making the code in the library readable. On this page we provide general +project. Good names provide concise descriptions of an entry's purpose, and help +making the code in the library readable. On this page we provide general guidelines for naming entries that apply anywhere in the library. -We also mention that the naming scheme of agda-unimath evolves as agda grows. +Accurately naming entries in a large formalization project can be very +difficult, especially when your formalization enters uncharted, or little +written about territory. Giving good names to your entries requires a high level +of conceptual understanding of your entries. The naming scheme should help +reveal common patterns in names, which hopefully helps to find predictable +namings for entries. On the other hand, we understand that this is not always +possible. If you find yourself not knowing what to name something, give it your +best shot to come up with a name, or reach out to us on the Univalent Agda +discord to ask if we have any suggestions. + +We also mention that the naming scheme of agda-unimath evolves as the library +grows. This implies that there are necessarily some inconsistencies in the +naming of our entries, even though we continually work to improve them. Sometimes we find that old namings don't fit our ideas of a good naming scheme -anymore, or we find other ways to improve on the naming. Some older code in the -library might even not be updated yet to fit the current naming scheme. We -should therefore remember that the naming scheme is not set in stone, and -maintaining and improving it is part of the work of maintaining the agda-unimath -library. - -Finally, we should note that accurately naming entries in a large formalization -project can be very difficult, especially when your formalization enters -unchartered, or little written about territory. Giving good names to your -entries requires a high level of conceptual understanding of your entries. The -naming scheme should help reveal common patterns in names, which hopefully helps -to find predictable namings for entries. On the other hand, we understand that -this is not always possible. If you find yourself not knowing what to name -something, give it your best shot to come up with a name, or reach out to us on -the Univalent Agda discord to ask if we have any suggestions. +anymore, or sometimes we gain a better understanding of what an entry is about +and update its name accordingly. We should therefore remember that neither the +naming scheme nor the names we use in the library are set in stone. If you find +a particular entry where the naming seems off, for any reason, we would love to +know about it. Maintaining and improving it is part of the work of maintaining +the agda-unimath library. ## Examples From 4ac7ec8a94f18454d43fc32dd01743b57f007169 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 13:44:05 +0200 Subject: [PATCH 16/33] update examples --- NAMING-CONVENTIONS.md | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index c8a1dbaa86..cd2274d551 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -29,7 +29,7 @@ the agda-unimath library. ## Examples -The library contains, for example, an entry `is-iso-hom-Ring` for the predicate +For example, the library has an entry named `is-iso-hom-Ring` for the predicate that a ring homomorphism is an isomorphsim. The most significant aspect of this predicate is the assertion that something is an isomorphism. Furthermore, we make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is @@ -41,13 +41,20 @@ construction's name and its type. Take, for example, the proof that the successor function on integers is an equivalence. It has the type `is-equiv succ-ℤ`, so we name it `is-equiv-succ-ℤ`. -We may also reflect the type of hypotheses used in the construction within the -name. If we wish to do so, we name the hypotheses after we have named the type -of the construction. For instance, `is-equiv-is-contr-map` is a function of type -`is-contr-map f → is-equiv f`, where `f` is a given function. Notice how the -term `is-equiv-is-contr-map H` places the descriptor `is-contr-map` right next -to the variable `H` it refers to. Another advantage is that the name says -immediately what it constructs. +We also consider the type of hypotheses when naming a construction. Typically, +when including hypotheses in the name, we mention them after the type of the +main construction. Let's take the entry `is-equiv-is-contr-map` as an example. +In this entry, we show that any +[contractible map](foundation.contractible-maps.md) is an +[equivalence](foundation.equivalences.md). The type of this entry is therefore +`is-contr-map f → is-equiv f`, where `f` is an assumed function. In the term +`is-equiv-is-contr-map H`, the descriptor `is-contr-map` is positioned adjacent +to its corresponding variable, `H`. Furthermore, by beginning the name with the +descriptor `is-equiv` we quickly see that this entry outputs proofs of +equivalence. + +By aligning names with types and incorporating hypotheses when relevant, the +naming scheme aims for clarity and predictability. ## The general scheme From cc82fac6db39908196997d7a8c28a66b315f4764 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 13:59:26 +0200 Subject: [PATCH 17/33] updating the general scheme --- NAMING-CONVENTIONS.md | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index cd2274d551..074e5aaf82 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -58,19 +58,28 @@ naming scheme aims for clarity and predictability. ## The general scheme -In general, our naming scheme follows the following pattern: +In general, our naming scheme follows the pattern: ```text [name]-[type]-[hypotheses]-[Namespace] ``` -We note that Agda has, as of yet, no namespace mechanism. This means that in -places where we wished to be able to use namespaces, we would append the name of -an entry with the name that we would have given to that namespace. We use this -naming convention for important mathematical concepts, such as groups, rings, -categories, graphs, trees, and so on. Furthermore, we note that in the general -naming scheme above all parts are optional, but the order of the different parts -of the name must be respected. +In this general pattern, all the components are optional. However, their order +is fixed and should be maintained for consistency. + +The general naming pattern breaks down as follows: + +- **[name]:** This part is used to give a custom descriptive name for the entry. +- **[type]:** This part of the name refers to the output type of the entry. +- **[hypotheses]:** This part of the name consists of descriptors for the + hypotheses used in the type specification of the entry. +- **[Namespace]:** This part of the name describes what important concept or + general category the entry is about. + +Given Agda's current lack of a namespace mechanism, we've incorporated what +would typically be a namespace directly into the name. This convention is +particularly applied to key mathematical concepts, such as groups, rings, +categories, graphs, and trees. ### Naming mathematical structures From e91085b27d596742c259b2eea53244dbbff533d6 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:14:40 +0200 Subject: [PATCH 18/33] incorporating some of Vojtech's comments --- CODING-STYLE.md | 9 ++++ NAMING-CONVENTIONS.md | 118 ++++++++++++++++++++---------------------- 2 files changed, 65 insertions(+), 62 deletions(-) diff --git a/CODING-STYLE.md b/CODING-STYLE.md index 3eda7c8c4d..015ee4e3ce 100644 --- a/CODING-STYLE.md +++ b/CODING-STYLE.md @@ -355,6 +355,15 @@ the story. Here's how we handle indentation and line breaks in the maintainability of the code, and you may find that it violates some of our other conventions as well. +- Using the projection functions `pr1` and `pr2`, particularly their + compositions, can lead to short code, but we recommend to avoid doing so. When + constructions contain a lot of projections throughout their definition, the + projections reveal little of what is going on in that part of the projections. + We therefore prefer naming the projections. When a type of the form `Σ A B` is + given a name, naming its projections too can enhance readability and will + provide more informative responses when jumping to the definition. + Furthermore, it makes it easier to change the definition later on. + - The use of `where` blocks in definitions is perfectly fine but keeping them short and specific to the definition of the current object is beneficial. Note that definitions made in a `where` block in a definition cannot be reused diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 074e5aaf82..5ebb49f8b0 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -13,8 +13,10 @@ of conceptual understanding of your entries. The naming scheme should help reveal common patterns in names, which hopefully helps to find predictable namings for entries. On the other hand, we understand that this is not always possible. If you find yourself not knowing what to name something, give it your -best shot to come up with a name, or reach out to us on the Univalent Agda -discord to ask if we have any suggestions. +best shot to come up with a name, or reach out to us on the +[Univalent Agda discord server](https://discord.gg/Zp2e8hYsuX) to ask if we have +any suggestions. One of the most commonly asked questions is what to name a +certain entry. We also mention that the naming scheme of agda-unimath evolves as the library grows. This implies that there are necessarily some inconsistencies in the @@ -61,7 +63,7 @@ naming scheme aims for clarity and predictability. In general, our naming scheme follows the pattern: ```text - [name]-[type]-[hypotheses]-[Namespace] + [descriptor]-[output-type]-[input-types]-[Namespace] ``` In this general pattern, all the components are optional. However, their order @@ -69,56 +71,63 @@ is fixed and should be maintained for consistency. The general naming pattern breaks down as follows: -- **[name]:** This part is used to give a custom descriptive name for the entry. -- **[type]:** This part of the name refers to the output type of the entry. -- **[hypotheses]:** This part of the name consists of descriptors for the - hypotheses used in the type specification of the entry. +- **[descriptor]:** This part is used to give a custom descriptive name for the + entry. +- **[output-type]:** This part of the name refers to the output type of the + entry. +- **[input-types]:** This part of the name consists of references to the input + types used in the type specification of the entry. - **[Namespace]:** This part of the name describes what important concept or general category the entry is about. -Given Agda's current lack of a namespace mechanism, we've incorporated what -would typically be a namespace directly into the name. This convention is +Given Agda's current lack of a namespace mechanism, we can't have named logical +collection of definitions that span multiple files. Instead, we've incorporated +what would typically be a namespace directly into the name. This convention is particularly applied to key mathematical concepts, such as groups, rings, -categories, graphs, and trees. +categories, graphs, and trees, and so on. ### Naming mathematical structures We saw, for example, that the prediate `is-iso-hom-Ring` has the part `Ring` capitalized. This signifies that the predicate is about rings. This name follows -the scheme `[name]-[hypotheses]-[Namespace]`. Note that there is also the entry -`is-iso-prop-hom-Ring`. This is a predicate that returns for each ring +the scheme `[descriptor]-[input-types]-[Namespace]`. Note that there is also the +entry `is-iso-prop-hom-Ring`. This is a predicate that returns for each ring homomorphism the _proposition_ that it is an isomorphism, and therefore it -follows the scheme `[name]-[type]-[hypotheses]-[Namespace]`. Now we can guess -what a construction named `hom-iso-Ring` should be about: It should be a -construction that constructs the underlying homomorphism of an isomorphisms of -rings. This name follows the pattern `[type]-[hypotheses]-[Namespace]`. - -There is also a common class of entries where we don't use the `[name]` part in -the name of an entry: underlying objects. For example, the underlying set of a -group is called `set-Group`, which uses the pattern `[type]-[Namespace]`. The -construction of the underlying set of a group returns for each group a set, -which is an element of type `Set`. Similarly, we have `type-Group]`, -`semigroup-Group`, `type-Ring`, `set-Ring`, and so on. Another instance where -this happens is in `hom-iso-Group`, which is the construction that returns the -underlying group homomorphism of an isomorphism of group. The fact that a group -isomorphism is an isomorphsim is called `is-iso-iso-Group`, which also uses the -pattern `[type]-[Namespace]`. One could also consider calling it -`is-iso-hom-iso-Group`, to emphasize that the underlying group homomorphism of -the isomorphism is an isomorphism. However, this name does not fit our patterns -in any way, and the addition of `hom` to the name adds no extra useful -information. This situation is common in instances where we omit the `[name]` -part of a name. For instance `is-category-Category` and `is-ideal-ideal-Ring` -follow the patterns `[type]-[Namespace]` and `[type]-[hypotheses]-[Namespace]`. +follows the scheme `[descriptor]-[output-type]-[input-types]-[Namespace]`. Now +we can guess what a construction named `hom-iso-Ring` should be about: It should +be a construction that constructs the underlying homomorphism of an isomorphisms +of rings. This name follows the pattern +`[output-type]-[input-types]-[Namespace]`. + +There is also a common class of entries where we don't use the `[descriptor]` +part in the name of an entry: underlying objects. For example, the underlying +set of a group is called `set-Group`, which uses the pattern +`[output-type]-[Namespace]`. The construction of the underlying set of a group +returns for each group a set, which is an element of type `Set`. Similarly, we +have `type-Group`, `semigroup-Group`, `type-Ring`, `set-Ring`, and so on. +Another instance where this happens is in `hom-iso-Group`, which is the +construction that returns the underlying group homomorphism of an isomorphism of +group. The fact that a group isomorphism is an isomorphsim is called +`is-iso-iso-Group`, which also uses the pattern `[output-type]-[Namespace]`. One +could also consider calling it `is-iso-hom-iso-Group`, to emphasize that the +underlying group homomorphism of the isomorphism is an isomorphism. However, +this name does not fit our patterns in any way, and the addition of `hom` to the +name adds no extra useful information. This situation is common in instances +where we omit the `[descriptor]` part of a name. For instance +`is-category-Category` and `is-ideal-ideal-Ring` follow the patterns +`[output-type]-[Namespace]` and `[output-type]-[input-types]-[Namespace]`, +respectively. Another class of entries where the naming scheme needs some explanation, is where we define a structured object from another structured object. For instance, the [kernel](group-theory.kernels.md) of a [group homomorphism](group-theory.homomorphisms-groups.md) is defined to be the [normal subgroup](group-theory.normal-subgroups.md) `kernel-hom-Group`. This -name follows the scheme `[name]-[hypotheses]-[Namespace]`. When we want to -define the underlying structure of the kernel of a group homomorphism, we follow -the scheme `[type]-[hypotheses]-[Namespace]`. For instance, the underlying group -of the kernel of a group homomorphism is called `group-kernel-hom-Group`. +name follows the scheme `[descriptor]-[input-types]-[Namespace]`. When we want +to define the underlying structure of the kernel of a group homomorphism, we +follow the scheme `[output-type]-[input-types]-[Namespace]`. For instance, the +underlying group of the kernel of a group homomorphism is called +`group-kernel-hom-Group`. ### Naming conventions for mathematical laws @@ -129,8 +138,8 @@ stated as `left-unit-law` and `right-unit-law`. The fact that [multiplication on the integers](elementary-number-theory.multiplication-integers.md) satisfies the unit laws is then stated as `left-unit-law-mul-ℤ` and `right-unit-law-mul-ℤ`. In the general naming scheme, this naming follows the -pattern `[type]-[Namespace]`, because it states the type of which an element is -constructed, and we treat `ℤ` as a namespace. +pattern `[output-type]-[Namespace]`, because it states the type of which an +element is constructed, and we treat `ℤ` as a namespace. For a second example, `interchange-law` states what it means to satisfy the [interchange law](foundation.interchange-law.md). This interchange law requires @@ -142,7 +151,7 @@ the same. For example, in the [integers](elementary-number-theory.integers.md) there is an interchange law for addition over addition, which states that `(a + b) + (c + d) ＝ (a + c) + (b + d)`. This law is called `interchange-law-add-add-ℤ`. Again, this naming follows the pattern -`[type]-[Namespace]`, because it states the type of which an element is +`[output-type]-[Namespace]`, because it states the type of which an element is constructed. ### Further naming conventions for operations on types @@ -191,11 +200,7 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. [full width equals sign](https://codepoints.net/U+ff1d) for the identity type, as the standard equals sign is a reserved symbol in Agda. -If you are unsure about what to name your entry, ask us on the Univalent Agda -discord server. One of the most commonly asked questions is what to name a -certain thing. - -## Naming conventions we try to avoid +## Naming practices we try to avoid - Abbreviations might seem like a good way to shorten names, but we use them sparingly. They might save a couple of keystrokes for the author, but in the @@ -212,23 +217,12 @@ certain thing. and not `commutative-×`, and the unit of a modality is called `unit-modality` and not `unit-○`. -- To enhance conceptual clarity, we suggest names of constructions avoid +- To improve conceptual clarity, we suggest names of constructions avoid referring to variable names. This makes code more understandable, even at a glance, and easier to work with in subsequent code. -- Using the projection functions `pr1` and `pr2`, particularly their - compositions, can lead to short code, but we recommend to avoid doing so. When - constructions contain a lot of projections throughout their definition, the - projections reveal little of what is going on in that part of the projections. - We therefore prefer naming the projections. When a type of the form `Σ A B` is - given a name, naming its projections too can enhance readability and will - provide more informative responses when jumping to the definition. - Furthermore, it makes it easier to change the definition later on. - -- Lastly, we recommend not naming constructions after infix notation of - operations included in them. Preferring primary prefix notation over infix - notation can help keep our code consistent. For example, it's preferred to use - `commutative-prod` instead of `commutative-×` for denoting the commutativity - of cartesian products. - -- Names never reference variables. +- Names never reference variables. For example, `G`-sets are called + [group actions](group-theory.group-actions.md) in our library. The type of all + group actions on a given group `G` is called `Abstract-Group-Action`. This + name also contains the prefix `Abstract` in order to disambiguate from + [concrete group actions](group-theory.concrete-group-actions.md). From 88a9226a92ec17d85d5e8b86ce12776c151d8dbf Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:29:02 +0200 Subject: [PATCH 19/33] Update NAMING-CONVENTIONS.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- NAMING-CONVENTIONS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 5ebb49f8b0..d8f3424202 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -81,7 +81,7 @@ The general naming pattern breaks down as follows: general category the entry is about. Given Agda's current lack of a namespace mechanism, we can't have named logical -collection of definitions that span multiple files. Instead, we've incorporated +collections of definitions that span multiple files. Instead, we've incorporated what would typically be a namespace directly into the name. This convention is particularly applied to key mathematical concepts, such as groups, rings, categories, graphs, and trees, and so on. From 74e06972960b2f1035f1b4dd5631bb910263e204 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:30:47 +0200 Subject: [PATCH 20/33] Update NAMING-CONVENTIONS.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- NAMING-CONVENTIONS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index d8f3424202..2787dc7bc4 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -84,7 +84,7 @@ Given Agda's current lack of a namespace mechanism, we can't have named logical collections of definitions that span multiple files. Instead, we've incorporated what would typically be a namespace directly into the name. This convention is particularly applied to key mathematical concepts, such as groups, rings, -categories, graphs, and trees, and so on. +categories, graphs, trees, and so on. ### Naming mathematical structures From a8bfc8fc416b3bbf1e05907a53360ed2aefd9569 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:47:10 +0200 Subject: [PATCH 21/33] Update NAMING-CONVENTIONS.md Co-authored-by: Fredrik Bakke --- NAMING-CONVENTIONS.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 2787dc7bc4..1c1dd3a6e2 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -31,7 +31,8 @@ the agda-unimath library. ## Examples -For example, the library has an entry named `is-iso-hom-Ring` for the predicate +Before we present a general scheme, let us first get a feel for the structure of names in agda-unimath by considering some examples. +The library has an entry named `is-iso-hom-Ring` for the predicate that a ring homomorphism is an isomorphsim. The most significant aspect of this predicate is the assertion that something is an isomorphism. Furthermore, we make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is From 6f882443ca53a1829a1dde9245f844dcdb464702 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:48:50 +0200 Subject: [PATCH 22/33] Update NAMING-CONVENTIONS.md Co-authored-by: Fredrik Bakke --- NAMING-CONVENTIONS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 1c1dd3a6e2..3a436fb74a 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -49,7 +49,7 @@ when including hypotheses in the name, we mention them after the type of the main construction. Let's take the entry `is-equiv-is-contr-map` as an example. In this entry, we show that any [contractible map](foundation.contractible-maps.md) is an -[equivalence](foundation.equivalences.md). The type of this entry is therefore +[equivalence](foundation-core.equivalences.md). The type of this entry is therefore `is-contr-map f → is-equiv f`, where `f` is an assumed function. In the term `is-equiv-is-contr-map H`, the descriptor `is-contr-map` is positioned adjacent to its corresponding variable, `H`. Furthermore, by beginning the name with the From fa770b4735a6265d0992cc103a03d8b2ddba02f4 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 16:50:20 +0200 Subject: [PATCH 23/33] make pre-commit --- NAMING-CONVENTIONS.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 3a436fb74a..71902e3bca 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -31,13 +31,13 @@ the agda-unimath library. ## Examples -Before we present a general scheme, let us first get a feel for the structure of names in agda-unimath by considering some examples. -The library has an entry named `is-iso-hom-Ring` for the predicate -that a ring homomorphism is an isomorphsim. The most significant aspect of this -predicate is the assertion that something is an isomorphism. Furthermore, we -make this assertion about ring homomorphisms. The name `is-iso-hom-Ring` is -therefore a logical name for the predicate that a ring homomorphism is an -isomorphism. +Before we present a general scheme, let us first get a feel for the structure of +names in agda-unimath by considering some examples. The library has an entry +named `is-iso-hom-Ring` for the predicate that a ring homomorphism is an +isomorphsim. The most significant aspect of this predicate is the assertion that +something is an isomorphism. Furthermore, we make this assertion about ring +homomorphisms. The name `is-iso-hom-Ring` is therefore a logical name for the +predicate that a ring homomorphism is an isomorphism. In our naming scheme we strive for a direct correspondence between a construction's name and its type. Take, for example, the proof that the @@ -49,11 +49,11 @@ when including hypotheses in the name, we mention them after the type of the main construction. Let's take the entry `is-equiv-is-contr-map` as an example. In this entry, we show that any [contractible map](foundation.contractible-maps.md) is an -[equivalence](foundation-core.equivalences.md). The type of this entry is therefore -`is-contr-map f → is-equiv f`, where `f` is an assumed function. In the term -`is-equiv-is-contr-map H`, the descriptor `is-contr-map` is positioned adjacent -to its corresponding variable, `H`. Furthermore, by beginning the name with the -descriptor `is-equiv` we quickly see that this entry outputs proofs of +[equivalence](foundation-core.equivalences.md). The type of this entry is +therefore `is-contr-map f → is-equiv f`, where `f` is an assumed function. In +the term `is-equiv-is-contr-map H`, the descriptor `is-contr-map` is positioned +adjacent to its corresponding variable, `H`. Furthermore, by beginning the name +with the descriptor `is-equiv` we quickly see that this entry outputs proofs of equivalence. By aligning names with types and incorporating hypotheses when relevant, the From 633b4711f6262a5b4dfaa51ea1cd5dd63e4182ce Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 17:01:39 +0200 Subject: [PATCH 24/33] Update NAMING-CONVENTIONS.md Co-authored-by: Fredrik Bakke --- NAMING-CONVENTIONS.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 71902e3bca..67202c658b 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -176,9 +176,9 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. - We use US English spelling of words in names. - When an entry is predominantly about objects of an important concept, the - names of these concepts can be capitalized. Usually, these are categories like + names of these concepts can be capitalized. Usually, these are categories in one way or another, like `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, `Preorder`, `Poset`, - `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, and so on. + `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, `Truncated-Type`, `Spectrum` and so on. - As a general rule of thumb, names should start out with an all lowercase portion with words separated by hyphens, and may have a capitalized portion at From bd3ed0bf9d5855e1d071445eeb70d64de2643615 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 17:02:35 +0200 Subject: [PATCH 25/33] make pre-commit --- NAMING-CONVENTIONS.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 67202c658b..baf58ffdcc 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -176,9 +176,10 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. - We use US English spelling of words in names. - When an entry is predominantly about objects of an important concept, the - names of these concepts can be capitalized. Usually, these are categories in one way or another, like - `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, `Preorder`, `Poset`, - `Precategory`, `Category`, `Directed-Graph`, `Undirected-Graph`, `Truncated-Type`, `Spectrum` and so on. + names of these concepts can be capitalized. Usually, these are categories in + one way or another, like `Prop`, `Set`, `Semigroup`, `Monoid`, `Group`, + `Preorder`, `Poset`, `Precategory`, `Category`, `Directed-Graph`, + `Undirected-Graph`, `Truncated-Type`, `Spectrum` and so on. - As a general rule of thumb, names should start out with an all lowercase portion with words separated by hyphens, and may have a capitalized portion at From 0b278163d02bb976582f7563a8986741a665f015 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 20:48:15 +0200 Subject: [PATCH 26/33] list of common descriptors --- NAMING-CONVENTIONS.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index baf58ffdcc..4cb056480a 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -167,6 +167,23 @@ library is `Ω`. Therefore, we record the function that transport computes to as `tr-Ω` and we record the [homotopy](foundation.homotopies.md) that transport is pointwise equal to `tr-Ω` as `compute-tr-Ω`. +## List of common descriptors + +In the table below we list some common descriptors that are not directly tied to +a type with that name. + +| Descriptor | Purpose | +| ---------------- | -------------------------------------------------------------------------------------------------------------- | +| `coh` | Used for proofs of coherence | +| `coherence` | Used to assert coherence | +| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | +| `Eq` | Used for identity systems on types of a particular form | +| `eq` | Used as a descriptor for the identity type | +| `extensionality` | Used for computations of identity types | +| `is-property` | Used when `is-prop` is unavailable | +| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | +| `type` | Used for the underlying type of an object | + ## Overview of our naming conventions - Names are unique; we steer clear of namespace overloading. From 63a009164fa78068a079ff7a4b6de033a85f5fee Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 21:05:10 +0200 Subject: [PATCH 27/33] Update NAMING-CONVENTIONS.md Co-authored-by: Fredrik Bakke --- NAMING-CONVENTIONS.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 4cb056480a..b7e5d30557 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -169,8 +169,7 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. ## List of common descriptors -In the table below we list some common descriptors that are not directly tied to -a type with that name. +To give a sense of the kind of general descriptors we use, we list some common descriptors in the table below. | Descriptor | Purpose | | ---------------- | -------------------------------------------------------------------------------------------------------------- | From 1f956426125801060495ee4f374d1fa1b949cf69 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 21:09:04 +0200 Subject: [PATCH 28/33] make pre-commit --- NAMING-CONVENTIONS.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index b7e5d30557..7ca56c98c9 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -169,7 +169,8 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. ## List of common descriptors -To give a sense of the kind of general descriptors we use, we list some common descriptors in the table below. +To give a sense of the kind of general descriptors we use, we list some common +descriptors in the table below. | Descriptor | Purpose | | ---------------- | -------------------------------------------------------------------------------------------------------------- | From fdea201a75c3430d68156b49dd1fbc4bbbc30cbe Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 22 Sep 2023 21:18:34 +0200 Subject: [PATCH 29/33] equiv and htpy in the table --- NAMING-CONVENTIONS.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 7ca56c98c9..623cc33f12 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -179,7 +179,9 @@ descriptors in the table below. | `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | | `Eq` | Used for identity systems on types of a particular form | | `eq` | Used as a descriptor for the identity type | +| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | | `extensionality` | Used for computations of identity types | +| `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types | | `is-property` | Used when `is-prop` is unavailable | | `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | | `type` | Used for the underlying type of an object | From 693cb0f2eb996c761709a3ba8dacc3d7fd3482e4 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 23 Sep 2023 14:10:25 +0200 Subject: [PATCH 30/33] work --- NAMING-CONVENTIONS.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 623cc33f12..efbf9a6436 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -72,13 +72,13 @@ is fixed and should be maintained for consistency. The general naming pattern breaks down as follows: -- **[descriptor]:** This part is used to give a custom descriptive name for the +- **\[descriptor\]:** This part is used to give a custom descriptive name for + the entry. +- **\[output-type\]:** This part of the name refers to the output type of the entry. -- **[output-type]:** This part of the name refers to the output type of the - entry. -- **[input-types]:** This part of the name consists of references to the input +- **\[input-types\]:** This part of the name consists of references to the input types used in the type specification of the entry. -- **[Namespace]:** This part of the name describes what important concept or +- **\[Namespace\]:** This part of the name describes what important concept or general category the entry is about. Given Agda's current lack of a namespace mechanism, we can't have named logical From 6006e808e0cf238784788cb2274abbe5079438b0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 23 Sep 2023 17:14:25 +0200 Subject: [PATCH 31/33] explaining the goals --- NAMING-CONVENTIONS.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index efbf9a6436..6b381c3954 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -6,6 +6,22 @@ project. Good names provide concise descriptions of an entry's purpose, and help making the code in the library readable. On this page we provide general guidelines for naming entries that apply anywhere in the library. +The naming conventions for the agda-unimath library are designed to be in line +with the overall goals of the project, which is to be an informative resource of +formalized mathematics. We therefore made the following list of priorities for +our naming conventions: + +- Entry names aim to concisely describe their mathematical concept, using + well-known mathematical vocabulary. +- While an entry's name reflects its concept, it avoids relying on the details + of its formalization. This way, a user is not required to know how something + is formalized in order to reference an entry. +- Even with only minimal knowledge of our conventions, users can intuitively + grasp an entry's purpose. +- Our naming scheme works across mathematical fields and throughout the library. +- Ultimately, our goal is for these conventions to support clear and + maintainable code. + Accurately naming entries in a large formalization project can be very difficult, especially when your formalization enters uncharted, or little written about territory. Giving good names to your entries requires a high level @@ -227,7 +243,8 @@ descriptors in the table below. sparingly. They might save a couple of keystrokes for the author, but in the grand scheme of things, they will likely compromise readability and maintainability, especially for newcomers and maintainers. We aim for clarity, - not brevity. + not brevity. We always keep the possibility in mind that abbreviations might + be confusing for someone. - Using Unicode characters in names is permissible, but we recommend restraint to maintain readability. Just a few well-placed symbols can often express a From 81f66b81a65510d8d72e72250bee93f41dba7a75 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 23 Sep 2023 17:21:04 +0200 Subject: [PATCH 32/33] predictability --- NAMING-CONVENTIONS.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 6b381c3954..2633fcba25 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -19,6 +19,8 @@ our naming conventions: - Even with only minimal knowledge of our conventions, users can intuitively grasp an entry's purpose. - Our naming scheme works across mathematical fields and throughout the library. +- For many common kinds of entries, our naming scheme offers a predictable + suggestion of what its name should be. - Ultimately, our goal is for these conventions to support clear and maintainable code. From fce34cda3ee6f24bafeb0a461ed25c7dc7030ee8 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 23 Sep 2023 17:28:30 +0200 Subject: [PATCH 33/33] clarify use of --- NAMING-CONVENTIONS.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 2633fcba25..adddd23b7a 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -190,19 +190,19 @@ pointwise equal to `tr-Ω` as `compute-tr-Ω`. To give a sense of the kind of general descriptors we use, we list some common descriptors in the table below. -| Descriptor | Purpose | -| ---------------- | -------------------------------------------------------------------------------------------------------------- | -| `coh` | Used for proofs of coherence | -| `coherence` | Used to assert coherence | -| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | -| `Eq` | Used for identity systems on types of a particular form | -| `eq` | Used as a descriptor for the identity type | -| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | -| `extensionality` | Used for computations of identity types | -| `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types | -| `is-property` | Used when `is-prop` is unavailable | -| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | -| `type` | Used for the underlying type of an object | +| Descriptor | Purpose | +| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `coh` | Used for proofs of coherence | +| `coherence` | Used to assert coherence | +| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | +| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system. `Eq` is commonly used as a descriptor for identity systems on number systems. | +| `eq` | Used as a descriptor for the identity type | +| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | +| `extensionality` | Used for computations of identity types | +| `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types | +| `is-property` | Used when `is-prop` is unavailable | +| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | +| `type` | Used for the underlying type of an object | ## Overview of our naming conventions