The following is an excerpt from DESIGN-PRINCIPLES.md:

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, 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. Adittionally, the replacement axiom can be proven by the join construction, which only uses pushouts. Finally, the Agda built-in types do not change the semantics of the theory, they only give convenience to the user of the library.

It would be nice if most of these assertions were formalized in the library and linked to from the design principles.

Concretely, the following statements can be formalized:

• The circle can be constructed as the type of ℤ-torsors.
• The replacement axiom can be used to prove there is a circle in UU lzero.
• The replacement axiom can be proven by the join construction.
  (This is Theorem 4.6 of Egbert's article The join construction (arXiv:1701.07538))

Similar to #664. To fix this, custom.js should probably use .gitignore to filter files.

Jonathan and I have been working together to try to define a ruleset for how import statements should be ordered, as he is developing a script to automate the sorting of these (#488 #487 #484).

The import order that we are currently proposing is the following.

1. public import statements
2. non-public Agda primitive imports
3. non-public import statements from the same namespace
4. non-public import statements from other namespaces
5. other open statements (this seems to be unconventional, but alas there are instances of this in the library)

Within these categories, the statements should be sorted alphabetically.

The reasoning is that this will hopefully correlate well with the relevance of each individual import, while still being somewhat intuitive to the user/contributor.

This file had an ill-typed <details> block which wasn't closed, but it wasn't detected by make pre-commit.

https://unimath.github.io/agda-unimath/finite-group-theory.transpositions-standard-finite-types.html

As demonstrated by #447, I think for the scalability of this project, there should be a job in the GitHub workflow that checks that the appropriate module references are in place, as it's a recurring and tedious job to manually do this.

What I have in mind is a script that checks the following:

• For every appropriate subdirectory, check that there is a .lagda.md file with the name of that subdirectory.
• For every file in that directory, check that it defines a module named supdirectory-name.[...].subdirectory-name.file-name (given that nested namespaces are allowed)
• In the subdirectory .lagda.md file, check that every .lagda.md file in the subdirectory is imported
• Check that each import is public
• Check that the imports in it are sorted alphabetically
• Check that there is a header in SUMMARY.lagda.md with a reference to every subdirectory's .lagda.md file
• Check that this header is the title inside that subdirectory's .lagda.md file
• Check that every file in that subdirectory is referenced in SUMMARY.lagda.md under that subdirectory
• Check that the name used to reference that file is the title inside the file
• Check that the entries are sorted in alphabetic order (either by the title in the file, or the name of the file)

Since we switched to the custom titles, entries starting with "The" are listed among pages starting with "T". This is wrong. For example, the page on the binomial theorem should be among the pages starting with "B", not with "T" even though the title of the page is "The binomial theorem".

Cmd+Opt+U displays the following error

[Error] Refused to execute https://unimath.github.io/agda-unimath/theme/images/agda-unimath-logo.svg as script because image/svg+xml is not a script MIME type.

There are certain molecules called allotropes of carbon which consist entirely of carbon atoms. Examples include carbon nanotubes and fullerines.
https://en.wikipedia.org/wiki/Allotropes_of_carbon
https://en.wikipedia.org/wiki/Carbon_nanotube
https://en.wikipedia.org/wiki/Fullerene
With the current definition of hydrocarbon, these molecules are hydrocarbons with zero hydrogen atoms.

But I'm not sure if the chemistry community would call allotropes of carbon 'hydrocarbons', common usage seems to imply that there is at least one hydrogen atom in a hydrocarbon.

Some of the pre-commit hooks, like generate_main_index_file.py, don't properly behave when the src folder is dirty. For instance when a MAlonzo folder is present. To fix this, we can filter out patterns from the .gitignore file.

We should decide on conventions for notation.

Right now every "eveluation" operation related to functors and natural isomorphisms has its own symbol. It would be better to have consistent naming scheme for them.

Click, for instance, in any reference to the name Level.

Not sure if I have bad clone or something, but my git checkout of this repo is over 500MB.
Which seems a little surprising, but maybe it really is that big?
(though the submodule to hott-set-theory is only 7.6MB)

If it's expected perhaps it is worth mentioning in the readme?

Following Emily Riehl, Jonathan Weinberger, and Nikolai Kudasov's example over at https://github.com/emilyriehl/yoneda, I think we should port to using <svg>s (scalable vector graphics) rather than ASCII diagrams, as these look wildly better and are far more versatile.

The original example I brought up on Discord can be seen here: https://emilyriehl.github.io/yoneda/simplicial-hott/05-segal-types.rzk/ (source: https://raw.githubusercontent.com/emilyriehl/yoneda/master/src/simplicial-hott/05-segal-types.rzk.md)
Screenshot:

And works flawlessly almost flawlessly flawlessly on our website as well when pasted over.
Example screenshot:

(Observe that the arrows are missing their heads. It seems they may have added some extra CSS code to get the arrowheads. Thanks to @VojtechStep for pointing out that this is because I failed to copy the code over properly.)

Please note that the positioning and scaling can be adjusted using simple inline XML and CSS snippets.

LaTeX is not rendered in the left-hand view, i.e. the numbered overview of namespaces and modules. This issue was detected a while back, and all instances were fixed in #639 by removing all latex code from module titles. However, if we want to have latex in module titles in the future, it would be nice if they were:

1. rendered properly in the left-hand view,

or at the very least, if

2. the dollar signs were not visible.

The latter would be a satisfactory fix, as long as we restrict ourselves to using Unicode characters as opposed to escaped latex codes.

Sorry, but I don't have an example to show you. Though, it should be easy enough to recreate by introducing LaTeX to a module title and building the website locally.

make pre-commit gives the following output, even on repeated runs:

Trim Trailing Whitespace.....................................................Passed
Fix End of Files.............................................................Passed
Mixed line ending............................................................Passed
Fix double quoted strings....................................................Passed
Check python ast.............................................................Passed
Check Yaml...................................................................Passed
Check for case conflicts.....................................................Passed
Check for merge conflicts....................................................Passed
Check for added large files..................................................Passed
Markdown conventions.........................................................Failed
- hook id: markdown-conventions
- exit code: 1

Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/markdown_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Blank line conventions in literate Agda Markdown files.......................Failed
- hook id: blank-line-conventions
- exit code: 1

Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/blank_line_conventions.py", line 6, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Format Agda imports..........................................................Failed
- hook id: fix-imports
- exit code: 1

Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/fix_imports.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Simple Agda space conventions................................................Failed
- hook id: spaces-conventions-simple
- exit code: 1

Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/spaces_conventions_simple.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Fix simply wrappable long lines of Agda code.................................Failed
- hook id: simply-wrappable-long-lines
- exit code: 1

Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable
Traceback (most recent call last):
  File "scripts/simply_wrappable_long_lines.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Check the maximum line length conventions....................................Failed
- hook id: max-line-length-conventions
- exit code: 1

Traceback (most recent call last):
  File "scripts/max_line_length_conventions.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Generate Agda namespace index modules........................................Failed
- hook id: generate-namespace-index-modules
- exit code: 1

Traceback (most recent call last):
  File "scripts/generate_namespace_index_modules.py", line 8, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Generate main index file.....................................................Failed
- hook id: generate-main-index-file
- exit code: 1

Traceback (most recent call last):
  File "scripts/generate_main_index_file.py", line 7, in <module>
    import utils
  File "/home/eriehl/Math/Hopkins/Formalization/agda-unimath/scripts/utils/__init__.py", line 21, in <module>
    def find_index(s: str, t: str) -> list[int]:
TypeError: 'type' object is not subscriptable

Python scripts formatting....................................................Passed
CSS, JS, YAML and Markdown (no codeblocks) formatting........................Passed
make: *** [Makefile:90: pre-commit] Error 1

This is inconvenient as it makes the process of building the website quite a bit longer. There are other steps in the process that ensure the library is type checked, so why insert it here as well? Having a library that type checks should not be necessary to build the website.

Some files erroneously end the details block with <details> instead of <\details>. However, I don't know the regular expression to search and replace this throughout the library. All occurrences of <details> followed by a new line character should be replaced by <\details>

Following a suggestion made by @jonaprieto (#627 (comment)) I'll record here an issue about potential ways to make our pre-commit hooks usable by third-parties.

It runs into universe problems, indicating that there is something off with the file. Some lemmas are extremely long, and it is also one of files that takes longest to compile.

Currently, the documentation pages respond with weird HTML when a non-existent page is accessed. See for instance here: https://unimath.github.io/agda-unimath/non-existent. It would be nice if it returned a standard 404 page instead.

I get the following error:

egbertrijke@MacBook-Pro-3 scripts % python update_contributors.py 
  File "update_contributors.py", line 9
    url = f'https://api.github.com/repos/{repo}/contributors'
                                                            ^
SyntaxError: invalid syntax

The cumulenes are a class of hydrocarbons with at least three consecutive pairs of double bonds between neighbouring carbon atoms. As a result, the carbon atoms in the middle of the chain of double bonds each have 4 carbon-carbon bonds.
https://en.wikipedia.org/wiki/Cumulene
Another example of a class of hydrocarbons with a carbon atom with 4 carbon-carbon bonds is any alkyne that is not acetylene:
https://en.wikipedia.org/wiki/Alkyne
If Amelia is correct that the current definition of hydrocarbon only allows carbon atoms to have at most 3 carbon-carbon bonds in #232 (comment), than the current definition excludes the cumulenes and the alkynes.

TODO

• #714
• Clean up commented code
• Clean up unused imports (?)
• #479
• Add symbol for coproducts
• Syntax for Id (?)
• Change name of src/README (?)
• Complete refactoring of synthetic homotopy theory
• Make sure all files conform to guidelines

It is pretty common for checks in a PR to go through, but then after a merge the website fails to build if there are broken links.

TODO

• Prove that mono-Concrete-Group is a set.
• Define the type of subgroups using G-sets.
• Prove that the two types are equivalent.
• Prove that hom-Concrete-Group is a set.
• Prove that mono-Concrete-Group are the monomorphisms in the category of concrete groups.

          Just noting that the library is not particularly consistent with respect to this convention currently.

Originally posted by @fredrik-bakke in #511 (comment)

We are getting the following error:

WARNING! Duplicate titles in elementary-number-theory:
[1165](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1166)
  Title 'Inequality on integer fractions': inequality-integer-fractions, inequality-rational-numbers
[1166](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1167)
  Title 'The rational numbers': rational-numbers, reduced-integer-fractions
[1167](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1168)
make: *** [SUMMARY.md] Error 2

Ideally, the CI would catch this when it checks a PR, but currently it doesn't catch these kinds of errors.

I have filed an issue with commonmark/commonmark-spec regarding this problem, so progress on this can be followed there: commonmark/commonmark-spec#731.

This was detected with EleonoreMangel's newest PR

• #521.

The hook remove_extra_blank_lines fails with an error message due to a missing ```agda tag (this is not something that can easily be automatically fixed), however, the error message is not passed on to the user.

As the title says. This would prevent introducing of broken links, for example.

Benzene is a molecule with 6 carbon atoms and 6 hydrogen atoms, where the carbon atoms are arranged in a manner such that the projection into 2-dimesnional space is a hexagon.

The current definition of hydrocarbon assumes that bonds between carbon atoms are either a single, double, or triple bond. However, due to quantum mechanics, the bonds between carbon atoms in a Benzene molecule are neither a single bond nor a double bond; instead the electrons that would otherwise have been involved in forming bonds instead become delocalised, and are no longer associated to a bond between two carbon atoms. This phenomena is called resonance in chemistry.
https://en.wikipedia.org/wiki/Resonance_(chemistry)

What is defined in this library is instead the Lewis structure of a hydrocarbon.
https://en.wikipedia.org/wiki/Lewis_structure
In hydrocarbons with resonance there are multiple Lewis structures associated with a hydrocarbon. The actual structure of a hydrocarbon could be said to be an average of all the Lewis structures of a hydrocarbon.

We might need to run a script or write our mdbook preprocessor to add this information to each webpage. See https://rust-lang.github.io/mdBook/for_developers/preprocessors.html#hints-for-implementing-a-preprocessor.

A possible approach to proving this fact is to first prove that the interval type $𝕀$ (defined in synthetic-homotopy-theory.interval-type) is a representing object for identifications, i.e.
$$A^𝕀 \simeq \sum_{(x,y:A)}(x=_Ay)$$
for all types $A$, and then use that it gives us a type to curry over, hence "pulling the identification out of the Π" by an equivalence. The currying equivalence is equiv-swap-Π in foundation.type-arithmetic-dependent-function-types.

The resulting proof should probably be named funext-𝕀 and be placed in a new section of synthetic-homotopy-theory.interval-type. Caution should be made not to accidentally invoke function extensionality somewhere in the proof by applying a lemma that relies on it.

For a reference, this fact is partially established in the HoTT book (Lemma 6.3.2 and Exercise 6.10).

For example, it didn't sort the imports here:
https://unimath.github.io/agda-unimath/finite-group-theory.transpositions-standard-finite-types.html

The problem

On the main page of the docs, when you scroll through all of the modules or follow a reference to a specific place in this index, it is not necessarily clear which namespace the given modules you're looking at are in, or even what the precise name of that module is.

Consider for instance

Two natural questions I repeatedly want a quick answer to here is:

1. Is this in the index of modules in foundation or foundation-core?
2. What's the module name for "Commuting 3-simplices of maps" for instance?

Two suggestions

To improve this, I propose two solutions

1. Have the module names in some less aggressive color such as light gray next to each index entry
2. Have the current namespace as a sticky header on the page.

An illustration incorporating both ideas:

Although it probably looks neater if the module names are aligned as well.

Construct the hopf fibration in such a way that the generator of $\mathbb{S}^3$ is sent to a 3-loop in $\mathbb{S}^2$ constructed using Eckmann-Hilton.

A detailed plan for this may be too much to write out in a comment here. But I'll list a few components that will go into this:

• finish dependent universal property of suspensions
• "Universal Property of Fibers of maps": build up infrastructure for working with the family of fibers of a map f : A --> B as the initial type family equipped with a section (a : A) --> fib_f (f a).
  Open tasks
• show EH is (more or less) the naturality condition of whiskering a 2-path on the left by a 1-path
• "Eckmann-Hilton in the universe" idea: show that tr sends EH on identifications to EH on homotopies (almost done, missing a few coherences)

Synthetic homotopy prereqs:

• descent for $\mathbb{S}^1$, $\mathbb{S}^2$, $\mathbb{S}^3$
  ----- related to issue #1122 . This proof works best the the point and n-loop presentation of spheres, which have yet to be postulated.
• characterizing (higher) homotopies between (homotopies) functions with domain $\mathbb{S}^1$,
• characterizing homotopies between dependent functions functions with domain $\mathbb{S}^3$.

Quasi-references:

• a talk presenting the current version of the proof https://morphismz.github.io/talks/2024-04-03-hottuf

Reading Agda blocks using a Dark theme (which is nice for your eyes) is hard.
The changes should be made in theme/Agda.css, preferably using vars from theme/css/variable.css. Ask if you want more details to help here.

The page https://unimath.github.io/agda-unimath/CITATION.html looks bad and should not be indexed. The markdown file is mainly there for the Cite this repository-button on GitHub.

I'm working on the equivalent definitions of countable types. I've proved is-countable implies is-countable'. For the other direction, there was an unfinished work in the previous version

module _
  {l : Level} (X : UU-Set l)
  where
{-
  is-countable-is-countable' :
    is-countable' X → is-countable X
  is-countable-is-countable' H =
    apply-universal-property-trunc-Prop H
      ( is-countable-Prop X)
      ( λ (P , f) →
        unit-trunc-Prop
          ( pair
            ( λ n →
              map-coprod
                ( λ { (zero-ℕ , p) → ex-falso p ;
                      (succ-ℕ n , p) → map-surjection f (n , p)})
                ( λ x → star)
                ( map-left-distributive-Σ-coprod ℕ
                  ( {!is-in-decidable-subtype ∘ ?!})
                  ( ¬ ∘ shift-ℕ empty (is-in-decidable-subtype P))
                  ( pair n
                    ( is-decidable-subtype-decidable-subtype
                      ( shift-ℕ empty-decidable-Prop P) {!!}))))
            {!!}))
            -}

-- ℕ → Σ (n : ℕ), P' n + ¬ (P' n)
--   → (Σ (n : ℕ), P' n) + (Σ (n : ℕ), ¬ (P' n))
--   → X + 1

-- P' := shift-ℕ ∅ P

I couldn't understand how we define ℕ → Σ (n : ℕ), P' n + ¬ (P' n). Do you have any suggestion/idea?

make pre-commit often gives an error on the first run, and then a second run is required which runs then without errors. It looks like this process could be streamlined (eg, always run twice?)

There's also have decide-leq-ℤ in inequality-integers. I'll rename these later today, they aren't used in many places.

I figured we could compile a list of operators and propose fixities and constraints on what should precede what if we indeed want to define this in the library.

Some of my initial suggestions are as follows.

Fixity

• Function composition should associate to the right.
  f ∘ g ∘ h means f ∘ (g ∘ h).
• Identification concatenation should associate to the left as concatenation is done in diagrammatic order.
  p ∙ q ∙ r means (p ∙ q) ∙ r.
• Homotopy concatenation should associate to the left as concatenation is done in diagrammatic order.
  p ∙h q ∙h r means (p ∙h q) ∙h r.
• Homotopy left whiskering should associate to the right.
  f ·l g ·l H only makes sense as f ·l (g ·l H).
  Although in this instance it would also make sense to just write (f ∘ g) ·l H.
• Homotopy right whiskering should associate to the left.
  H ·r g ·r f only makes sense as (H ·r g) ·r f.
• Products and coproducts should associate to the right.
  A × B × C means A × (B × C), and A + B + C means A + (B + C).
• Identity and homotopy type formation should not associate to either side.
  x ＝ y ＝ z is ambiguous, f ~ g ~ h is always ill-typed.

Precedence

• Function composition, homotopy concatenation, homotopy left whiskering, and homotopy right whiskering should have precedence over identity and homotopy type formation.
  E.g. f ∘ g ~ h means (f ∘ g) ~ h.
• Identification concatenation should have precedence over identity type formation.
  p ∙ q ＝ r means (p ∙ q) ＝ r.
• Identification concatenation, homotopy concatenation, homotopy left whiskering, and homotopy right whiskering should have the same precedence.
• Function composition should have the same precedence level as homotopy concatenation, and homotopy right whiskering.
  e.g. H ∙h K ∘ f and H ·r g ∘ f are ambiguous (note that this is not an issue with left whiskering).
• Homotopy type formation could have precedence over identity type formation,
  as f ~ g ＝ X only ever makes sense as (f ~ g) ＝ X since functions cannot be homotopic to types.
• Products should have precedence over, or the same precedence, as coproducts.
  e.g. A × B + C means (A × B) + C or is ambiguous.
• The operator _∘_ may have precedence over _,_, as the alternative is always ill-typed.
  e.g. f , g ∘ h means f , (g ∘ h).

There's a make target to install the website dependencies, assuming you have Rust installed (it uses cargo): make install-website-dev. Then to build the website you run make website, and to open it you run make serve-website (it takes a second to start the web server, and IIRC then it should open up the page in your browser automatically).
This should probably be documented somewhere.

Originally posted by @VojtechStep in #622 (comment)

In #549 @ElifUskuplu reported that make pre-commit gave her the following error:

Executable `scripts/remove_extra_blank_lines.py` not found

The first middle-dot is · ("MIDDLE DOT", codepoint #xb7), and it's used in left and right whiskering (_·l_ and _·r_ in foundation-core.homotopies).
The other one is ∙ ("BULLET OPERATOR", codepoint #x2219), and it's used in the same file for homotopy concatenation, just a few lines above left and right whiskering.

To my knowledge, the middle dot can't even be typed using agda-input.

From a cursory look through the output of greping for MIDDLE DOT, it's only used for these two whiskering operators and some prose in groups and rings. Perhaps these occurences should be replaced by the other symbol?

The documentation and various make targets are inconsistent between using python vs python3 and pip vs pip3. This can lead to confusion as these don't necessarily point to the same executables. For instance if the user installs the required packages with pip and then runs make pre-commit, it is not guaranteed that the proper requirements are installed. We should decide on using either one, and use that consistently everywhere.

Git should ignore everything.lagda.md, but we want to keep it on the website.

In markdown, sometimes you want to add double white space in order to add a line break. For example, if you write a list

1. One item

   Something to say further about it
2. Second item
3. Third item

The most markdown renderers will add extra space between all list items. This is not always desirable. One way to mitigate this problem is to write the list in the following way:

1. One item  
   Something to say further about it
2. Second item
3. Third item

Note that there are two additional spaces after "1. One item ". This double white-space tells markdown to add a line break, because the line break that you see in the code actually doesn't suffice to add it. However, our double white-space remover removes these, so it is impossible to use this solution. My suggestion is to let the double white-space remover act only within agda code blocks.

When clicking the "cite this repository" button in the about panel on the main page of our repository, I get the message

Your CITATION.cff file cannot be parsed. Make sure the formatting is correct.