Created on 2023-03-03.
Last modified on 2023-11-24.
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
--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
- The function extensionality axiom is postulated in
- The univalence axiom is postulated in
- The type theoretic replacement axiom is postulated in
- The truncation operations are postulated in
- The interval is postulated in
- The circle is postulated in
- Pushouts are postulated in
- Various Agda built-in types are postulated in
- The flat modality and accompanying modalities, with propositional
computation rules, are postulated in
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
ℤ-torsors, and the
replacement axiom can be used to prove there is a
UU lzero. Additionally, the replacement axiom can be proven by the
join construction, which only uses
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
and would welcome contributions in that direction.
- The source code of the formalization can be found in the folder
- 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.
agda-unimathlibrary 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
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
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.
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).
- 2023-06-22. Egbert Rijke and Fredrik Bakke. Clarify conventions (#511).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).
- 2023-03-19. Fredrik Bakke. Updated installation guide and some additions to the VSCode workspace (#514).