diff --git a/CITE-THIS-LIBRARY.md b/CITE-THIS-LIBRARY.md index 060016e665..43d4fe9e4d 100644 --- a/CITE-THIS-LIBRARY.md +++ b/CITE-THIS-LIBRARY.md @@ -1,4 +1,4 @@ -# Citing the `agda-unimath` library +# Citing the agda-unimath library If you wish to reference our library in your work, please use the following BibTeX entry: diff --git a/CITING-SOURCES.md b/CITING-SOURCES.md index 228603293b..70342d44b3 100644 --- a/CITING-SOURCES.md +++ b/CITING-SOURCES.md @@ -31,7 +31,7 @@ not available, please define them as empty fields. E.g. `publisher = {},`. If you are unsure about how to structure your BibLaTeX entry, it may be useful to know that the references are checked by the `linkcheck` GitHub workflow, so -when you post your pull request to `agda-unimath` you can refer to the CI for +when you post your pull request to agda-unimath you can refer to the CI for possible issues. **Note:** If the citation label of your reference is not being generated diff --git a/CODINGSTYLE.md b/CODINGSTYLE.md index 8bf8b8409c..857677b8c2 100644 --- a/CODINGSTYLE.md +++ b/CODINGSTYLE.md @@ -1,6 +1,6 @@ -# The `agda-unimath` library style guide +# The agda-unimath library style guide -The `agda-unimath` library is an ever-expanding encyclopedia of formalized +The agda-unimath library is an ever-expanding encyclopedia of formalized mathematics from a univalent point of view. The library's corresponding website serves as an extensive platform, presenting our work in a structured, encyclopedia-like format. @@ -13,16 +13,16 @@ thereby weaving each contribution into a bigger tapestry. Conceptual clarity and readability are the core values of our formalization project. This style guide aims to help contributors write code that is both functional and understandable, as well as easily maintainable. Please reach out -to us if you have any questions or remarks about the `agda-unimath` style, or -need any help getting started with your formalization project. Our code, and -also this guide, are open to refinement to best support our community and the +to us if you have any questions or remarks about the agda-unimath style, or need +any help getting started with your formalization project. Our code, and also +this guide, are open to refinement to best support our community and the project's goals. ## Code structuring conventions -The `agda-unimath` library is a comprehensive collection of formalized -mathematics spanning a broad range of subjects. All fields of mathematics are -inherently interlinked, which we leverage in our formalization process. +The agda-unimath library is a comprehensive collection of formalized mathematics +spanning a broad range of subjects. All fields of mathematics are inherently +interlinked, which we leverage in our formalization process. One critical aspect of maintaining such a large codebase lies in efficient and strategic code structuring, and continued refactoring, into small, reusable @@ -62,17 +62,17 @@ Here are the benefits of this approach: In essence, our code structuring conventions are guided by the goal of ensuring that our code remains as conceptually clear and as understandable as possible. Finally, a maintainable codebase is a welcoming codebase. By ensuring that the -`agda-unimath` code is easy to understand and navigate, new contributors can -more readily participate in the project. This is crucial for the growth and -dynamism of the `agda-unimath` community. It allows a diverse group of -developers, each with their unique skills and perspectives, to contribute to the -project's ongoing success. +agda-unimath code is easy to understand and navigate, new contributors can more +readily participate in the project. This is crucial for the growth and dynamism +of the agda-unimath community. It allows a diverse group of developers, each +with their unique skills and perspectives, to contribute to the project's +ongoing success. So, in particular, refactoring isn't just about "cleaning up" the code; it's a strategic endeavour to ensure the longevity, vitality, and success of the -`agda-unimath` project. +agda-unimath project. -## Guidelines for definitions in the `agda-unimath` library +## Guidelines for definitions in the agda-unimath library - **Universe polymorphism**: We make use of universe polymorphism to make our definitions maximally applicable. Each assumed type or type family is assigned @@ -173,10 +173,10 @@ strategic endeavour to ensure the longevity, vitality, and success of the ## Code comments -Given that the files in `agda-unimath` are literate Agda markdown files, -designed to be displayed in a user-friendly format on the `agda-unimath` -website, we have the opportunity to comment on our code using markdown outside -of the code blocks. +Given that the files in agda-unimath are literate Agda markdown files, designed +to be displayed in a user-friendly format on the agda-unimath website, we have +the opportunity to comment on our code using markdown outside of the code +blocks. Each code block typically starts with a section header that provides a succinct explanation of the code's purpose or functionality. This header can be followed @@ -216,8 +216,8 @@ module _ The use of descriptive section headers, coupled with comprehensive markdown explanations, allows readers to gain a conceptual understanding of the code's -purpose, and contributes towards making `agda-unimath` an informative resource -of formalized mathematics from a univalent point of view. +purpose, and contributes towards making agda-unimath an informative resource of +formalized mathematics from a univalent point of view. Note that in the process of writing comments for code, the question may come up whether an anonymous module can extend across multiple code blocks and their @@ -232,12 +232,12 @@ across too many code blocks. Note that for consistency across the library, our convention is to use US English in comments and other explanatory or introductory texts. -## Modules in the `agda-unimath` library +## Modules in the agda-unimath library Modules play an important role in structuring Agda code. They allow us to group related functions and definitions, increasing the readability and maintainability of our codebase. Here are our guidelines for using modules in -the `agda-unimath` library: +the agda-unimath library: - In Agda, every file should start by opening a module with the same name as the file. Generally, this should be the only named module in the file. Any @@ -346,11 +346,11 @@ 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. -## Formatting: Indentation, line breaks, and parentheses { #formatting } +## Formatting: indentation, line breaks, and parentheses { #formatting } Code formatting is like punctuation in a novel - it helps readers make sense of -the story. Here's how we handle indentation and line breaks in the -`agda-unimath` library: +the story. Here's how we handle indentation and line breaks in the agda-unimath +library: - In Agda, each definition is structured like a tree, where each operation can be seen as a branching point. We use indentation levels and parentheses to @@ -399,7 +399,7 @@ the story. Here's how we handle indentation and line breaks in the tree structure of the definition, and aligns well with our convention to have two-space indentation level increases. -- In order to improve the readability on the `agda-unimath` website, we use a +- In order to improve the readability on the agda-unimath website, we use a standard line length of 80 characters. There are only a few exceptions that enable us to have names that are more than 80 characters long: @@ -481,7 +481,7 @@ the story. Here's how we handle indentation and line breaks in the reusable definitions leads to more readable, maintainable, and also refactorable code. It can even help Agda's verification process run smoother. -- Record types aren't frequently used in the `agda-unimath` library. This is +- Record types aren't frequently used in the agda-unimath library. This is mostly because they make it more complex to characterize their identity type. However, when the identity type isn't as critical, feel free to use record types as they can be convenient. @@ -502,6 +502,6 @@ the story. Here's how we handle indentation and line breaks in 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 +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, beautiful, reusable, and maintainable. Happy coding! diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index a8639cfa87..ada849d7b3 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -1,8 +1,8 @@ # Library design principles Understanding the design principles, structure, and philosophy behind the -`agda-unimath` library is essential for effectively navigating and contributing -to it. This document aims to provide a clear and concise introduction. +agda-unimath library is essential for effectively navigating and contributing to +it. This document aims to provide a clear and concise introduction. ## Postulates and assumptions @@ -40,19 +40,19 @@ Note that there is some redundancy in the postulates we assume. For example, the [univalence axiom implies function extensionality](foundation.univalence-implies-function-extensionality.md), but we still assume function extensionality separately. Furthermore, [the interval type is contractible](synthetic-homotopy-theory.interval-type.md), -and the higher inductive types in the `agda-unimath` library only have -computation rules up to identification, so there is no need at all to postulate -it. The [circle](synthetic-homotopy-theory.circle.md) can be constructed as the -type of `ℤ`-[torsors](group-theory.torsors.md), and the +and the higher inductive types in the agda-unimath library only have computation +rules up to identification, so there is no need at all to postulate it. The +[circle](synthetic-homotopy-theory.circle.md) can be constructed as the type of +`ℤ`-[torsors](group-theory.torsors.md), and the [replacement axiom](foundation.replacement.md) can be used to prove there is a circle in `UU lzero`. Additionally, the replacement axiom can be proven by the join construction, which only uses [pushouts](synthetic-homotopy-theory.pushouts.md). -With these postulates, the `agda-unimath` library is a library for constructive +With these postulates, the agda-unimath library is a library for constructive univalent mathematics. Mathematics for which the law of excluded middle or the -axiom of choice is necessary is not yet developed in `agda-unimath`. However, we -are also open to any development of classical mathematics within `agda-unimath`, +axiom of choice is necessary is not yet developed in agda-unimath. However, we +are also open to any development of classical mathematics within agda-unimath, and would welcome contributions in that direction. ## Library structure @@ -61,14 +61,14 @@ and would welcome contributions in that direction. 2. The library is organized by mathematical subject, with one folder per subject. For each folder, there is also an Agda file of the same name, which lists the files in that folder by importing them publicly. -3. The `agda-unimath` library aims to be an informative resource for formalized +3. The agda-unimath library aims to be an informative resource for formalized mathematics. We therefore formalize in literate Agda using markdown, treating files as pages of a mathematics wiki. 4. Each file is focused on a single topic, typically introducing one new concept and establishing its basic properties, or proving a central theorem and deriving immediate corollaries thereof. -## Design philosophy of `agda-unimath` +## Design philosophy of agda-unimath When a person is searching for something in a library of formalized mathematics, they likely have a clear idea of the concept they are looking for. However, it @@ -76,15 +76,15 @@ is unlikely that they know all the other concepts on which the desired concept depends. Even if the concept they are seeking is an instance of something more general, we cannot assume that they are aware of this. We certainly don't expect users to have any knowledge of how their concept has been formalized in order to -find it in `agda-unimath`. In fact, users might have limited knowledge about the +find it in agda-unimath. In fact, users might have limited knowledge about the concept they're searching for, knowing only its name, and they may be seeking more information about it. In such cases, the ideal scenario is for them to easily locate their concept in a hyperlinked index, similar to the index found at the back of a book. This way, they can find the concept, click on it, and access the information they were looking for. -Concepts are given prominence in the `agda-unimath` library because users know -how to search for them. An index of the formalized concepts in `agda-unimath` is +Concepts are given prominence in the agda-unimath library because users know how +to search for them. An index of the formalized concepts in agda-unimath is created by listing the files in the library, with the file names serving as the indexing terms. To assist users in quickly finding the topics they are interested in, each file in our library focuses narrowly on a single concept, a @@ -115,7 +115,7 @@ does not account for the initial bootstrapping process at the foundational level of the library. To resolve these cyclic dependencies, we created two folders for the foundation -of the `agda-unimath` library: the `foundation-core` folder containing the basic +of the agda-unimath library: the `foundation-core` folder containing the basic setup, and the `foundation` folder containing all the components belonging to the library's foundation. The `foundation-core` folder contains files that are paired with files of the same name in the `foundation` folder. The corresponding diff --git a/GRANT-ACKNOWLEDGEMENTS.md b/GRANT-ACKNOWLEDGEMENTS.md index fb14868b2a..616726cbdb 100644 --- a/GRANT-ACKNOWLEDGEMENTS.md +++ b/GRANT-ACKNOWLEDGEMENTS.md @@ -1,6 +1,6 @@ # Grant acknowledgements -If you are doing significant work for the `agda-unimath` library, such as work +If you are doing significant work for the agda-unimath library, such as work that leads to a preprint, or a conference or journal submission, then we can also acknowledge any research grants you are working under on this page. diff --git a/HOME.md b/HOME.md index 22935d7e51..3c319b3bbe 100644 --- a/HOME.md +++ b/HOME.md @@ -1,7 +1,7 @@ # The agda-unimath library -Welcome to the `agda-unimath` project. This is a community-driven effort aimed -at formalizing mathematics from a univalent point of view using the dependently +Welcome to the agda-unimath project. This is a community-driven effort aimed at +formalizing mathematics from a univalent point of view using the dependently typed programming language [Agda](https://github.com/agda/agda). @@ -17,20 +17,20 @@ potential to be useful, and informative resources for both working and learning mathematicians. Our library is designed to work towards this goal, and we welcome contributions to the library within any topic in mathematics. -The `agda-unimath` library is compatible with Agda 2.6.4 and can be compiled by +The agda-unimath library is compatible with Agda 2.6.4 and can be compiled by running `make check` from the root directory of the repository. Learn more about using the library locally in our [installation guide](HOWTO-INSTALL.md). -## Participating in the Project +## Participating in the project -If you are interested in contributing to the `agda-unimath` project, we -encourage you to join the conversation in our +If you are interested in contributing to the agda-unimath project, we encourage +you to join the conversation in our [Univalent Agda discord server](https://discord.gg/Zp2e8hYsuX). This is a -discussion platform shared between the 1Lab, `agda-unimath`, Cubical Agda, and +discussion platform shared between the 1Lab, agda-unimath, Cubical Agda, and TypeTopology communities, where we are more than happy to get you started. To contribute, fork the library and create a separate branch for your work. Follow the instructions in our [installation guide](HOWTO-INSTALL.md) to set up the project. After you have completed your formalization, submit it via a pull request. We will review your contribution and work towards incorporating it into -the `agda-unimath` library. +the agda-unimath library. diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md index bc02d23bbd..546f092848 100644 --- a/HOWTO-INSTALL.md +++ b/HOWTO-INSTALL.md @@ -4,7 +4,7 @@ ### Quick setup -To work or experiment with the `agda-unimath` library on your machine, you will +To work or experiment with the agda-unimath library on your machine, you will need to have `agda` version 2.6.4 installed, and a suitable editor such as [Emacs](https://www.gnu.org/software/emacs/) or [Visual Studio Code](https://code.visualstudio.com/). The following instructions @@ -16,7 +16,7 @@ will help you on your way right away: ### Setup for contributors -In order to contribute to the `agda-unimath` library you will additionally need: +In order to contribute to the agda-unimath library you will additionally need: 1. `git` 2. `make` @@ -97,7 +97,7 @@ to adjust the remote addresses of your clone. ### Creating a branch within your clone of the library Once you've cloned the library, we highly recommend you to preserve the `master` -branch in its original state and up to date with the official `agda-unimath` +branch in its original state and up to date with the official agda-unimath repository. This means you should avoid making changes directly to the `master` branch. @@ -122,7 +122,7 @@ working branches when necessary. ## Installing Agda {#installing-agda} -The `agda-unimath` library is built and verified with Agda 2.6.4, and we provide +The agda-unimath library is built and verified with Agda 2.6.4, and we provide two methods for installation: with or without the package manager [Nix](https://nixos.org/). Nix streamlines the installation of Agda and its dependencies, providing a consistent and reproducible environment for the @@ -159,8 +159,8 @@ provided on the Agda documentation page. We recommend either [Emacs](https://www.gnu.org/software/emacs/) or [Visual Studio Code](https://code.visualstudio.com/) (VSCode) as your editor -when working with the `agda-unimath` library. Both editors offer support for -Agda development, and the choice between them is largely a matter of personal +when working with the agda-unimath library. Both editors offer support for Agda +development, and the choice between them is largely a matter of personal preference. Below, you'll find setup instructions for each editor to help you configure your preferred environment. @@ -183,9 +183,9 @@ opening Emacs outside the project. #### Literate Agda files -The `agda-unimath` library is written in literate markdown Agda. Add the -following line to your `.emacs` file to enable Emacs to handle literate Agda -files with the `.lagda.md` extension: +The agda-unimath library is written in literate markdown Agda. Add the following +line to your `.emacs` file to enable Emacs to handle literate Agda files with +the `.lagda.md` extension: ```elisp (setq auto-mode-alist (cons '("\\.lagda.md$" . agda2-mode) auto-mode-alist)) @@ -193,7 +193,7 @@ files with the `.lagda.md` extension: #### Special symbols -The `agda-unimath` library employs two notations for the identity type: +The agda-unimath library employs two notations for the identity type: Martin-Löf's original notation `Id` and an infix notation `_＝_`. The infix notation's equals sign is not the standard one, but rather the [full width equals sign](https://codepoints.net/U+ff1d). Observe that the full @@ -215,7 +215,7 @@ 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 +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 programming environment and on our website. To display a vertical ruler marking @@ -229,7 +229,7 @@ to your `.emacs` file. ### VSCode -The `agda-unimath` library comes with a predefined VSCode workspace. Open the +The agda-unimath library comes with a predefined VSCode workspace. Open the folder main repository folder in VSCode, and it should automatically recognize the workspace and apply the appropriate settings. @@ -298,14 +298,14 @@ in the library. ## Creating a setup for contributors {#contributor-setup} We welcome and appreciate contributions from the community. If you're interested -in contributing to the `agda-unimath` library, you can follow the instructions +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 [design principles](DESIGN-PRINCIPLES.md). ### Pre-commit hooks and Python dependencies -The `agda-unimath` library includes [pre-commit](https://pre-commit.com/) hooks +The agda-unimath library includes [pre-commit](https://pre-commit.com/) hooks that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of some rule violations in your commits, and for most violations they will also automatically apply the required changes. diff --git a/PROJECTS.md b/PROJECTS.md index ea664f4461..58f6c90135 100644 --- a/PROJECTS.md +++ b/PROJECTS.md @@ -1,9 +1,9 @@ -# Projects using the `agda-unimath` library +# Projects using the agda-unimath library -Here is a list of projects that use the `agda-unimath` library: +Here is a list of projects that use the agda-unimath library: - - -If your project uses the `agda-unimath` library, let us know, so we can add your +If your project uses the agda-unimath library, let us know, so we can add your project to the list. diff --git a/README.md b/README.md index 2261a4c59a..3da239be43 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # ![The agda-unimath library](https://github.com/UniMath/agda-unimath/assets/1252282/cbd9b67e-581c-41c7-bc1e-34862127bad2) -The `agda-unimath` library is a community formalization project for univalent +The agda-unimath library is a community formalization project for univalent mathematics in [Agda](https://github.com/agda/agda). The library project was created by Elisabeth Stenholm, Jonathan Prieto-Cubides, and Egbert Rijke, and is currently being maintained by Egbert Rijke, Fredrik Bakke, and Vojtěch diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py index 729649ef3f..cb4f95adcf 100755 --- a/scripts/generate_main_index_file.py +++ b/scripts/generate_main_index_file.py @@ -105,7 +105,7 @@ def generate_index(root_path): - [Maintainers](MAINTAINERS.md) - [Contributors](CONTRIBUTORS.md) - [Statement of inclusivity](STATEMENT-OF-INCLUSION.md) - - [Projects using Agda-Unimath](PROJECTS.md) + - [Projects using agda-unimath](PROJECTS.md) - [Grant acknowledgements](GRANT-ACKNOWLEDGEMENTS.md) - [Guides](HOWTO-INSTALL.md) - [Installing the library](HOWTO-INSTALL.md) diff --git a/src/foundation/global-choice.lagda.md b/src/foundation/global-choice.lagda.md index f90d012be0..dde44fdbc8 100644 --- a/src/foundation/global-choice.lagda.md +++ b/src/foundation/global-choice.lagda.md @@ -38,7 +38,7 @@ Global-Choice l = (A : UU l) → ε-operator-Hilbert A ## Properties -### The global choice principle is inconsistent in `agda-unimath` +### The global choice principle is inconsistent in agda-unimath ```agda abstract diff --git a/src/foundation/whiskering-operations.lagda.md b/src/foundation/whiskering-operations.lagda.md index 8ead624e9d..f43d3e1cc5 100644 --- a/src/foundation/whiskering-operations.lagda.md +++ b/src/foundation/whiskering-operations.lagda.md @@ -40,7 +40,7 @@ with respect to `μ` is an operation The general notion of whiskering is introduced in order to establish a clear naming scheme for all the variations of whiskering that exist in the -`agda-unimath` library: +agda-unimath library: 1. In [whiskering identifications with respect to concatenation](foundation.whiskering-identifications-concatenation.md) diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 0604f765e2..ed335c6155 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -62,7 +62,7 @@ satisfying the following four conditions The type of {{#concept "Dedekind real numbers" Agda=ℝ}} is the type of all Dedekind cuts. The Dedekind real numbers will be taken as the standard -definition of the real numbers in the `agda-unimath` library. +definition of the real numbers in the agda-unimath library. ## Definition diff --git a/theme/index.hbs b/theme/index.hbs index 229d9a0d1b..44975ea210 100644 --- a/theme/index.hbs +++ b/theme/index.hbs @@ -12,6 +12,26 @@ {{/if}} + + + + + + + {{> head}}