Minor search engine optimizations (#1197)

Adds some structured data markup/open graph tags providing some extra
information to search engines and for building link previews of the
website. Also standardizes the display form/capitalization of
"agda-unimath".

#1194

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:

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

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!

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,30 +61,30 @@ 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
 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

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.
 

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).
 
 <a href="https://github.com/unimath/agda-unimath">
@@ -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.