Library design principles
Created on 2023-03-03.
Last modified on 2024-10-09.
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.
Postulates and assumptions
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
data
types 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
primitives
and 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.
Library structure
- 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.
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
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.
Recent changes
- 2024-10-09. Fredrik Bakke. Extensionality of globular types (#1190).
- 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).