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.
The library assumes the --without-K and --exact-split flags of Agda and
makes use of several postulates.
- We make full use of Agda's
datatypes for introducing inductive types. - We make full use of Agda's universe levels, including
ω. However, it should be noted that most of the type constructors only define types of universe levels belowω, so a lot of the theory developed in this library does not apply to universe levelωand beyond. - The function extensionality axiom is postulated in
foundation.function-extensionality. - The univalence axiom is postulated in
foundation.univalence. - The type theoretic replacement axiom is postulated in
foundation.replacement - The truncation operations are postulated in
foundation.truncations - The interval is postulated in
synthetic-homotopy-theory.interval-type - The circle is postulated in
synthetic-homotopy-theory.circle - Pushouts are postulated in
synthetic-homotopy-theory.pushouts - Extensionality of globular types is postulated in
structured-types.equality-globular-types. - Various Agda built-in types are postulated in
primitivesand inreflection. - The flat modality and accompanying modalities, with propositional
computation rules, are postulated in
modal-type-theory.
Note that there is some redundancy in the postulates we assume. For example, the
univalence axiom implies function extensionality,
but we still assume function extensionality separately. Furthermore,
the interval type is contractible,
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 can be constructed as the type of
ℤ-torsors, and the
replacement axiom 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.
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, and would welcome contributions in that direction.
- The source code of the formalization can be found in the folder
src. - 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.
- 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.
- 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.
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 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 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 named theorem, or a specific topic. The file names succinctly and naturally describe the concept, theorem, or topic.
This organizational choice for the library allows us to structure our files in a manner similar to pages on a wiki. The file's title represents the topic at hand, and in an informal section, we can describe the main idea in words. Subsequently, we provide the main definition, the basic infrastructure surrounding it, and derive properties or consequences that hold with the same generality as the main definition of the file.
For instance, the file about sets initially defines what a set is, and then proceeds to demonstrate that sets are closed under equivalences, dependent pair types, dependent product types, and so on. However, it does not prove that the type of natural numbers is a set because users would more likely expect such information to be presented on the page specifically dedicated to natural numbers.
Let's consider a thought experiment. Suppose we have an unorganized library of mathematics and organize everything by topic as described above. Mathematics is already a well-organized subject, so this is our preferred way to organize most of the library. However, towards the bottom of the library, we encounter a cluster of interdependent files, and Agda will report errors due to these cyclic dependencies. The reason is that our desire to organize the library by topic 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
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
file in the foundation folder publicly imports the file from the
foundation-core folder. Users working in areas outside of the foundation can
directly import files from the foundation folder without worrying about
potential file splits.
Outside of the foundation folder, the library adheres to the design principle
of "one-concept-per-file." However, if you discover that something you were
looking for is located in a different place than expected (which can happen!),
please let us know, and we will consider it for future improvements.