The agdaunimath
library style guide
Created on 20230303.
Last modified on 20230912.
The agdaunimath
library is an everexpanding 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,
encyclopedialike format.
The coding and style conventions we've established aren't simply rules; they're tools for us to shape and nurture this resource. They ensure that the formalized definitions are clean and focused, and ready for reuse across the library, 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 agdaunimath
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 agdaunimath
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 entries. In line with this approach, we aim to factor out and encapsulate even the tiniest bits of reusable logic or computation in their own definitions.
Here are the benefits of this approach:

Simplicity: Breaking down complex structures into smaller ones simplifies the overall codebase, making it more accessible to new contributors.

Reusability: Once a particular logic or computation is formalized, it can be reused in multiple places, thereby avoiding redundancy and promoting efficiency.

Cleanliness: By separating reusable logic from proof constructions, we keep our proofs clean and focus only on the essential parts of the argument.

Demonstrability: Wellstructured code serves as a practical guide on how to use prior parts of the library in the current setting or in new definitions.

Maintainability: When logic is broken down into separate, reusable pieces, it becomes easier to manage and maintain the codebase. Constructions that are broken down into small definitions are much easier to understand. This also makes the project more scalable.

Reliability: While formally verified code is guaranteed to be "correct" in terms of its internal logic, it doesn't necessarily ensure that a mathematical concept is accurately modeled within Agda. By proving properties, reusing existing implementations in manners that mirror the expectations of mathematicians, and by tightly integrating them with the rest of the library, we create more opportunities to use and confirm the fidelity of these implementations. This process bolsters confidence in their correctness and the overall reliability of the library.
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
agdaunimath
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 agdaunimath
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
agdaunimath
project.
Guidelines for definitions in the agdaunimath
library

Universe polymorphism: We make use of universe polymorphism to make our definitions maximally applicable. Each assumed type or type family is assigned its own universe level.

Reuse of definitions: We advocate for the reuse of existing constructions in both type specifications and definition bodies. This not only helps maintain naming consistency, but also highlights the correlation between current and prior definitions, while keeping our code concise and to the point.

Comprehensive infrastructure for key concepts: To further elucidate the usage and scope of each concept in the library, we often invest in building comprehensive infrastructure around it. This approach not only clarifies the intent behind the definition but also helps keeping a consistent naming scheme by providing names for frequently used projections and other readily inferrable definitions. The emphasis on infrastructure enhances the library's maintainability since modifications to wellsupported definitions can be executed more easily than those lacking robust infrastructure. This is another way we endeavor to ensure the clarity, resilience, and continual evolution of our codebase. Good examples of files where infrastructure is welldeveloped include
grouptheory.groups
andgraphtheory.undirectedgraphs
. 
Implicit arguments: If an argument can be inferred in most use cases, make it implicit.

Use of anonymous modules: If several arguments are commonly used across different proofs, extract them into an anonymous module. This helps keep type specifications brief and ensures consistency in the variable ordering among related definitions.

Use of
where
blocks: Whilewhere
blocks are permissible, their use is generally discouraged as their content cannot be reused outside the main definition. This contradicts our objective of organizing the library into compact, reusable components. If awhere
block is deemed necessary, follow these conventions: Opt for
where
blocks overlet
expressions.  Indent the
where
keyword by two spaces and align their content with thewhere
keyword.  Position the
where
keyword on the line beneath the main proof, indented by two spaces.  Ensure each term has a type, and place all terms on lines following the
where
keyword. For instance:
statement : Statement statement = somepossiblylongproof a where a : typeofa a = constructionofa
 Opt for
Code comments
Given that the files in agdaunimath
are literate Agda markdown files,
designed to be displayed in a userfriendly format on the agdaunimath
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 by a more detailed exposition of the code, elucidating the primary concepts and methodologies used.
As an example, the page on joins of radical ideals contains the following explanation of the code that is about to follow:
### Products of radical ideals distribute over joins
Consider a radical ideal `I` and a family of radical ideals `J_α` indexed by
`α : U`. To prove distributivity, we make the following calculation where we
will write `·r` for the product of radical ideals and `⋁r` for the join of a
family of radical ideals.
```text
I ·r (⋁r_α J_α) ＝ √ (I · √ (⋁_α J_α))
＝ √ (I · (⋁_α J_α))
＝ √ (⋁_α (I · J_α))
＝ √ (⋁_α √ (I · J_α))
＝ ⋁r_α (I ·r J_α)
```
The proof below proceeds by proving inclusions in both directions along the
computation steps above.
```agda
module _
{l1 l2 l3 l4 : Level} (A : CommutativeRing l1)
(I : radicalidealCommutativeRing l2 A)
{U : UU l3} (J : U → radicalidealCommutativeRing l4 A)
where
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 agdaunimath
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 comments in between. This is indeed possible. We recommend, however, that modules should not extend over markdown section headers of any level. The sections and subsections in markdown are typically used to focus on a specific definition, property, or example, and in this case it is good to start a new anonymous module to display the context for the topic of that section. Furthermore, it helps the maintainability of the library if modules don't extend 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 agdaunimath
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 agdaunimath
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 additional modules should either be anonymous, or they should occur in the form of
record
ordata
definitions. 
However, we encourage the use of anonymous modules for grouping constructions that share a common theme or common parameters. Here is an example from
graphtheory.directedgraphs
:DirectedGraph : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) DirectedGraph l1 l2 = Σ (UU l1) (λ V → V → V → UU l2) module _ {l1 l2 : Level} (G : DirectedGraph l1 l2) where vertexDirectedGraph : UU l1 vertexDirectedGraph = pr1 G edgeDirectedGraph : (x y : vertexDirectedGraph) → UU l2 edgeDirectedGraph = pr2 G

We recommend leaving a single blank line after a module declaration for clarity and readability.

Module variables should be declared on a new line, with an indentation level increase of two spaces. If the variables cannot fit on a single line, they can be declared over multiple lines.

The
where
keyword should be positioned on a new line following the variable declarations, and it should also adopt the same twospace indentation level increase. 
If necessary, nested modules may be used. However, we recommend using them carefully and only when really needed. With nested modules it can sometimes be harder for readers as well as maintainers to keep track of assumptions.

Module imports should occur directly after the file's named module declaration and should be listed in alphabetical order to simplify navigation. Note that our
precommit
hooks automatically organize the imports; the user does not need to sort them by hand. 
The library doesn't use variables at the moment. All variables are declared either as parameters of an anonymous module or in the type specification of a construction.
Naming conventions
One of the key strategies to make our library easy to navigate is our naming
convention. We strive for a direct correspondence between a construction's name
and its type. Take, for instance, the proof that the successor function on
integers is an equivalence. It has the type isequiv succℤ
, so we name it
isequivsuccℤ
. Note how we prefer lowercase and use hyphens to separate
words.
We also reflect the type of hypotheses used in the construction within the name.
However, the crux of a name primarily describes the type of the constructed
term; descriptions of the hypotheses follow this. For instance,
isequiviscontrmap
is a function of type iscontrmap f → isequiv f
,
where f
is a given function. Notice how the term isequiviscontrmap H
places the descriptor iscontrmap
right next to the variable H
it refers
to.
While abbreviations might seem like a good way to shorten names, we use them sparingly. They might save a couple of keystrokes for the author, but in the grand scheme of things, they will likely compromise readability and maintainability, especially for newcomers and maintainers. We aim for clarity, not brevity.
Here is a list of our naming conventions:

Names are unique; we steer clear of namespace overloading.

Names should accurately convey the concept of its construction.

We use US English spelling of words in names.

Important concepts can be capitalized. Usually, these are categories like
Prop
,Set
,Semigroup
,Monoid
,Group
,Preorder
,Poset
,Precategory
,Category
,DirectedGraph
,UndirectedGraph
, and so on. 
As a general rule of thumb, names should start out with an all lowercase portion with words separated by hyphens, and may have a capitalized portion at the end that describes which larger mathematical framework the definition takes place in  for instance, if it is constructed internally to a certain subuniverse or category of mathematical objects.

The start of a name describes the object that is being constructed. For some theorems, the latter part of a name describes the hypotheses.

Names never reference variables.

We use Unicode symbols sparingly and only when they align with established mathematical practice.

Just as we do with abbreviations, we use special symbols sparingly in names.

If a symbol is not available, we describe the concept concisely in words.

We prioritize the readability of the code and avoid subtly different variations of the same symbol. An important exception is the use of the full width equals sign for the identity type, as the standard equals sign is a reserved symbol in Agda.
Formatting: Indentation, line breaks, and parentheses
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
agdaunimath
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 highlight this structure, which makes the code feel more organized and understandable. For example, when a definition part extends beyond a line, we introduce line breaks at the earliest branching point, clearly displaying the tree structure of the definition. This allows the reader to follow the branches of the tree, and to visually grasp the scope of each operation and argument. Consider the following example from
foundationcore.truncatedtypes
:module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where istruncequivistrunc : (k : 𝕋) → istrunc k A → istrunc k B → istrunc k (A ≃ B) istruncequivistrunc k H K = istruncΣ ( istruncfunctiontype k K) ( λ f → istruncΣ ( istruncΣ ( istruncfunctiontype k H) ( λ g → istruncΠ k (λ y → istruncId K (f (g y)) y))) ( λ _ → istruncΣ ( istruncfunctiontype k H) ( λ h → istruncΠ k (λ x → istruncId H (h (f x)) x))))
The root here is the function
istruncΣ
. It has two arguments, each starting on a fresh line with two extra spaces of indentation. The first argument fits neatly on one line, but the second one spills over. In these cases, we add a line break right after the→
symbol following the lambdaabstraction, which is the earliest branching point in this case. The next node is againistruncΣ
, with two arguments. Neither of them fits on a line, so we add a line break immediately. This process is continued until the definition is complete.Note also that we use parentheses to mark the branches. The extra space after the opening parentheses marking a branch is there to visually emphasize the tree structure of the definition, and aligns well with our convention to have twospace indentation level increases.

In order to improve the readability on the
agdaunimath
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: Named
module
declarations open import
statements Lines consisting of a single, possibly parenthesized (
(){}
), token that is potentially followed by one of the symbols;
,:
,=
, or→
.
 Named

The contents of a toplevel module have zero indentation. For every subsequent nested scope, we add an extra two spaces of indentation, so the indentation level should always be a multiple of two.

We always declare the variables of a module on a new line, with the indentation level increased by two spaces. If the variable declarations themselves spill over the 80 character line limit, we break them up with line breaks while grouping the variables together logically. The
where
keyword of a module declaration is entered on a new line after the variable declarations. 
If a construction's name and its type declaration do not fit into a single line, we move the type declaration to a new line with an extra two spaces of indentation. If the type specification still doesn't fit on an 80character line, we break it up across lines, keeping the same indentation level.

Some proofs contain a part with equational reasoning. The standard way to typeset equational reasoning proofs is as follows
equationalreasoning term1 ＝ term2 by equation1 ＝ term3 by equation2
Sometimes, however,
equationn
is a short proof term that fits on the same line asby
within the 80 character limit. In that case it is ok to do so. 
Expressions involving mixfix operators are appropriately parenthesized when the particular association bears relevance, or if there is any chance of confusion from omitting the parentheses. A reader of the code should not be expected to know the precedence levels or associativity of particular operators.
Coding practices we tend to avoid

Using Unicode characters in names is entirely permissible, but we recommend restraint to maintain readability. Just a few wellplaced symbols can often express a lot.

To enhance conceptual clarity, we suggest names of constructions avoid referring to variable names. This makes code more understandable, even at a glance, and easier to work with in subsequent code.

We encourage limiting the depth increase of indentation levels to two spaces. This practice tends to keep our code readerfriendly, especially on smaller screens, by keeping more code on the lefthand side of the screen. In particular, we discourage the use of indentation for the sole purpose of aligning code to make it "neat". In our experience, this hurts the maintainability of the code, and you may find that it violates some of our other conventions as well.

The use of
where
blocks in definitions is perfectly fine but keeping them short and specific to the definition of the current object is beneficial. Note that definitions made in awhere
block in a definition cannot be reused outside of that definition, and finding a way to factor out small lemmas into 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
agdaunimath
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. 
Using the projection functions
pr1
andpr2
, particularly their compositions, can lead to short code, but we recommend to avoid doing so. When constructions contain a lot of projections throughout their definition, the projections reveal little of what is going on in that part of the projections. We therefore prefer naming the projections. When a type of the formΣ A B
is given a name, naming its projections too can enhance readability and will provide more informative responses when jumping to the definition. Furthermore, it makes it easier to change the definition later on. 
Lastly, we recommend not naming constructions after infix notation of operations included in them. Preferring primary prefix notation over infix notation can help keep our code consistent. For example, it's preferred to use
commutativeprod
instead ofcommutative×
for denoting 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 agdaunimath
library are
valued, and these suggestions are here to help ensure that your code is clear,
beautiful, reusable, and maintainable. Happy coding!
Recent changes
 20230912. Egbert Rijke. guide for anonymous modules across multiple code blocks (#760).
 20230910. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
 20230625. Fredrik Bakke. Fix alignment
where
blocks (#670).  20230622. Egbert Rijke and Fredrik Bakke. Clarify conventions (#511).
 20230503. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).