diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 94db54052b..d57b3cd3aa 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -118,13 +118,22 @@ jobs:
crate: mdbook-linkcheck
version: '0.7.7'
+ # Install Python and friends for website generation only where needed
+ - uses: actions/setup-python@v4
+ with:
+ python-version: '3.8'
+ check-latest: true
+ cache: 'pip'
+
+ - run: python3 -m pip install -r master/scripts/requirements.txt
+
- uses: actions/cache/restore@v3
with:
key: pre-website-${{ github.run_id }}
path: master/docs
# Tell mdbook to use only the linkcheck backend
- - name: Check website links
+ - name: Check website links and bibtex references
env:
MDBOOK_OUTPUT: '{"linkcheck":{}}'
run: |
diff --git a/.vscode/settings.json b/.vscode/settings.json
index c4b4244f33..b7b45dc06a 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -106,6 +106,9 @@
"[python]": {
"editor.tabSize": 4,
- "editor.defaultFormatter": "ms-python.python"
+ "editor.defaultFormatter": null,
+ "editor.formatOnSave": false,
+ "editor.formatOnType": false,
+ "editor.formatOnPaste": false
}
}
diff --git a/CITING-SOURCES.md b/CITING-SOURCES.md
new file mode 100644
index 0000000000..09519bd9bc
--- /dev/null
+++ b/CITING-SOURCES.md
@@ -0,0 +1,41 @@
+# Citing sources
+
+All of the references and sources of the agda-unimath library are managed in a
+[BibLaTeX](https://www.ctan.org/pkg/biblatex) file `references.bib`, and we have
+a custom set of macros to work with them.
+
+The macros are as follows:
+
+
+
+- `{{#cite referenceXYZ}}` will insert a citation to the reference labeled
+ `referenceXYZ` (which must be defined in the `references.bib` file) at the
+ current location, and add that reference to the current page's bibliography.
+- `{{#reference referenceXYZ}}` will add the reference labeled `referenceXYZ`
+ to the current page's bibliography without inserting a citation.
+- `{{#bibliography}}` is a marker for where the bibliography of the current
+ page should be inserted. If no such marker is found and the bibliography is
+ inhabited, it will be inserted at the bottom of the page in a new section
+ titled `References`.
+
+Note that entries in the BibLaTeX file are expected to have all of the
+apropriate fields defined according to their type. For instance, `@book`s _must_
+have a defined field for `publisher` and `year`. If this information is not
+available, please define them as empty fields. E.g. `publisher = {},`.
+
+If you are unsure about how to structure your BibLaTeX entry, it may be useful
+to know that the references are checked by the `linkcheck` GitHub workflow, so
+when you post your pull request to `agda-unimath` you can refer to the CI for
+possible issues.
+
+**Note:** If the citation label of your reference is not being generated
+properly, we support a custom `citeas` field that can be used to overwrite it.
+For instance, _Homotopy Type Theory: Univalent Foundations of Mathematics_
+should be cited as {{#cite UF13}}, and to make it so we have set
+`citeas = {UF13}` for its BibLaTeX entry. Keep in mind that if the citation
+label is not being generated properly, then it is likely that the author list is
+not being parsed properly either.
diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
index 9d1e1b108a..bc02d23bbd 100644
--- a/HOWTO-INSTALL.md
+++ b/HOWTO-INSTALL.md
@@ -21,8 +21,8 @@ In order to contribute to the `agda-unimath` library you will additionally need:
1. `git`
2. `make`
3. `python` version 3.8 or newer
-4. The python libraries `pre-commit`, `requests` and `tomli`. Those can be
- installed by running
+4. The python libraries `pre-commit`, `pybtex`, `requests` and `tomli`. Those
+ can be installed by running
```shell
python3 -m pip install -r scripts/requirements.txt
```
diff --git a/Makefile b/Makefile
index 1e3e7e479d..003f3341e6 100644
--- a/Makefile
+++ b/Makefile
@@ -34,6 +34,7 @@ TIME ?= time
METAFILES := \
ART.md \
CITE-THIS-LIBRARY.md \
+ CITING-SOURCES.md \
CODINGSTYLE.md \
CONTRIBUTING.md \
CONTRIBUTORS.md \
@@ -49,7 +50,7 @@ METAFILES := \
STATEMENT-OF-INCLUSION.md \
SUMMARY.md \
TEMPLATE.lagda.md \
- USERS.md \
+ USERS.md
.PHONY: agdaFiles
agdaFiles:
diff --git a/TEMPLATE.lagda.md b/TEMPLATE.lagda.md
index 407fdace78..f178dcf0db 100644
--- a/TEMPLATE.lagda.md
+++ b/TEMPLATE.lagda.md
@@ -50,9 +50,3 @@ concept-subconcept = ...
- An instructive example of a file with the expected structure is
[`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).
-
-## References
-
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
diff --git a/book.toml b/book.toml
index 4ed9b191ee..206b2b5041 100644
--- a/book.toml
+++ b/book.toml
@@ -51,6 +51,14 @@ output-file = "docs/concept_index.json"
mathswitch-template = "https://mathswitch.xyz/concept/Wd/{wikidata_id}"
wikidata-template = "https://www.wikidata.org/entity/{wikidata_id}"
+[preprocessor.citations]
+command = "python3 ./scripts/preprocessor_citations.py"
+bibtex_file = "references.bib"
+citation_style = "alpha"
+citation_label_style = "custom_alpha"
+error_on_unmatched_keys = true
+before = [ "git-metadata" ]
+
[output.linkcheck]
follow-web-links = false
@@ -62,6 +70,7 @@ additional-css = [
"website/css/Agda.css",
"website/css/Agda-highlight.css",
"website/css/agda-logo.css",
+ "website/css/bibliography.css",
"theme/catppuccin.css",
"theme/catppuccin-admonish.css",
"theme/pagetoc.css",
diff --git a/flake.nix b/flake.nix
index a7c3ea3045..eecc477004 100644
--- a/flake.nix
+++ b/flake.nix
@@ -24,6 +24,7 @@
python = pkgs.python38.withPackages (p: with p; [
# Keep in sync with scripts/requirements.txt
# pre-commit <- not installed as a Python package but as a binary below
+ pybtex
requests
tomli
]);
diff --git a/references.bib b/references.bib
new file mode 100644
index 0000000000..6e9796dc04
--- /dev/null
+++ b/references.bib
@@ -0,0 +1,606 @@
+@article{AKS15,
+ title = {Univalent Categories and the {{Rezk}} Completion},
+ author = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
+ year = {2015},
+ month = {06},
+ journal = {Mathematical Structures in Computer Science},
+ volume = {25},
+ number = {5},
+ pages = {1010--1039},
+ issn = {0960-1295, 1469-8072},
+ doi = {10.1017/S0960129514000486},
+ abstract = {We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.},
+ eprint = {1303.0584},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ langid = {english}
+}
+
+@online{BCDE21,
+ title = {Free groups in HoTT/UF in Agda},
+ author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},
+ year = {2021},
+ url = {https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html}
+}
+
+
+@online{BCFR23,
+ title = {Central {{H-spaces}} and Banded Types},
+ author = {Buchholtz, Ulrik and Christensen, J. Daniel and Flaten, Jarl G. Taxerås and Rijke, Egbert},
+ year = {2023},
+ month = {02},
+ date = {2023-02-27},
+ eprint = {2301.02636},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ abstract = {We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own self-equivalences. From centrality alone we construct an infinite delooping in terms of a tensor product of banded types, which are the appropriate notion of torsor for a central type. Our constructions are carried out in homotopy type theory, and therefore hold in any $\infty$-topos. Even when interpreted into the $\infty$-topos of spaces, our main results and constructions are new. Along the way, we further develop the theory of H-spaces in homotopy type theory, including their relation to evaluation fibrations and Whitehead products. These considerations let us, for example, rule out the existence of H-space structures on the $2n$-sphere for $n {$>$} 0$. We also give a novel description of the moduli space of H-space structures on an H-space. Using this description, we generalize a formula of Arkowitz-Curjel and Copeland for counting the number of path components of this moduli space. As an application, we deduce that the moduli space of H-space structures on the $3$-sphere is $\Omega^6 \mathbb{S}^3$.},
+ pubstate = {preprint},
+ keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic}
+}
+
+@online{BDR18,
+ title = {Higher {{Groups}} in {{Homotopy Type Theory}}},
+ author = {Buchholtz, Ulrik and {{van}} Doorn, Floris and Rijke, Egbert},
+ citeas = {BDR18},
+ date = {2018-02-12},
+ year = {2018},
+ month = {02},
+ eprint = {1802.04315},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ abstract = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
+ pubstate = {preprint},
+ keywords = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
+}
+
+@online{BJR24,
+ title = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}},
+ author = {Buchholtz, Ulrik and {{de}} Jong, Tom and Rijke, Egbert},
+ citeas = {BJR24},
+ date = {2024-01-25},
+ year = {2024},
+ month = {01},
+ eprint = {2401.14106},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ abstract = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.},
+ pubstate = {preprint},
+ keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory}
+}
+
+@book{BSCS05,
+ title = {Absztrakt algebrai feladatok},
+ author = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes},
+ url = {https://interkonyv.hu/konyvek/balintne-szendrei-maria-czedli-gabor-szendrei-agnes-absztrakt-algebrai-feladatok/},
+ year = {2005},
+ publisher = {Polygon},
+ pagetotal = {523},
+ langid = {hungarian}
+}
+
+@article{BW23,
+ title = {Synthetic Fibered $(\infty,1)$-Category Theory},
+ author = {Buchholtz, Ulrik and Weinberger, Jonathan},
+ eprint = {2105.01724},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ year = {2023},
+ month = {05},
+ pages = {74-165},
+ volume = {7},
+ journal = {Higher Structures},
+ doi = {10.21136/HS.2023.04},
+ abstract = {We study cocartesian fibrations in the setting of the synthetic $(\infty,1)$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.},
+ pubstate = {preprint},
+ keywords = {03B38 18N60 18N45 18D30 18N55 55U35 18N50 18D40 18D70,Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic}
+}
+
+@article{CORS20,
+ title = {Localization in {{Homotopy Type Theory}}},
+ author = {Christensen, J. Daniel and Opie, Morgan and Rijke, Egbert and Scoccola, Luis},
+ date = {2020-02-09},
+ year = {2020},
+ month = {02},
+ eprint = {1807.04155},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ journal = {Higher Structures},
+ shortjournal = {High.Struct.},
+ volume = {4},
+ number = {1},
+ pages = {1--32},
+ doi = {10.21136/HS.2020.01},
+ url = {http://articles.math.cas.cz/10.21136/HS.2020.01},
+ issn = {2209-0606},
+ mrclass = {18E35 (03B38 18N45)},
+ mrnumber = {4074272},
+ mrreviewer = {J\'{e}r\^{o}me\ Scherer},
+ abstract = {We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural map $X \to X_{(p)}$ induces algebraic localizations on all homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L'$. Furthermore, we prove results establishing that $L'$ is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space $K(G,n)$ with $G$ abelian. We also include a partial converse to the main theorem.},
+ keywords = {55P60 (Primary) 18E35 03B15 (Secondary),Mathematics - Algebraic Topology,Mathematics - Category Theory}
+}
+
+@article{CR21,
+ title = {Modal Descent},
+ author = {Cherubini, Felix and Rijke, Egbert},
+ date = {2021-04},
+ year = {2021},
+ month = {04},
+ eprint = {2003.09713},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ journal = {Mathematical Structures in Computer Science},
+ volume = {31},
+ number = {4},
+ pages = {363--391},
+ issn = {0960-1295, 1469-8072},
+ doi = {10.1017/S0960129520000201},
+ abstract = {Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated with any modality, of which the left class is the class of $○$-equivalences and the right class is the class of $○$-étale maps. This factorization system is called the modal reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the modal reflective factorization system of a modality. In the special case of the $n$-truncation, the modal reflective factorization system has a simple description: we show that the $n$-étale maps are the maps that are right orthogonal to the map $\mathbf{1} \to \mathbf{S}^{n+1}$. We use the $○$-étale maps to prove a modal descent theorem: a map with modal fibers into $○X$ is the same thing as a $○$-étale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remark how $○$-étale maps relate to the formally étale maps from algebraic geometry.},
+ langid = {english},
+ keywords = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory}
+}
+
+@online{Dlicata335/Cohesion-Agda,
+ title = {Dlicata335/Cohesion-Agda},
+ author = {Licata, Dan},
+ date = {2017-11-06T03:09:02Z},
+ origdate = {2017-11-06T03:08:45Z},
+ url = {https://github.com/dlicata335/cohesion-agda},
+ howpublished = {{{GitHub}} repository}
+}
+
+@article{EKMS93,
+ title = {A {{Primer}} on {{Galois Connections}}},
+ author = {Erné, M. and Koslowski, J. and Melton, A. and Strecker, G. E.},
+ year = {1993},
+ journal = {Annals of the New York Academy of Sciences},
+ volume = {704},
+ number = {1},
+ pages = {103--125},
+ issn = {1749-6632},
+ doi = {10.1111/j.1749-6632.1993.tb52513.x},
+ abstract = {The rudiments of the theory of Galois connections (or residuation theory, as it is sometimes called) are provided, together with many examples and applications. Galois connections occur in profusion and are well known to most mathematicians who deal with order theory; they seem to be less known to topologists. However, because of their ubiquity and simplicity, they (like equivalence relations) can be used as an effective research tool throughout mathematics and related areas. If one recognizes that a Galois connection is involved in a phenomenon that may be relatively complex, then many aspects of that phenomenon immediately become clear, and thus, the whole situation typically becomes much easier to understand.},
+ langid = {english},
+ keywords = {axiality,closure operation,Galois connection,interior operation,polarity}
+}
+
+@online{Esc19DefinitionsEquivalence,
+ title = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
+ author = {Escardó, Martín Hötzel},
+ date = {2019-09-12},
+ year = {2019},
+ month = {09},
+ url = {https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ},
+ howpublished = {{{Google}} groups forum discussion}
+}
+
+@article{Esc21,
+ title = {The {{Cantor}}–{{Schröder}}–{{Bernstein Theorem}} for $\infty$-Groupoids},
+ author = {Escardó, Martín Hötzel},
+ date = {2021-09-01},
+ year = {2021},
+ month = {09},
+ eprint = {2002.07079},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ journal = {Journal of Homotopy and Related Structures},
+ shortjournal = {J. Homotopy Relat. Struct.},
+ volume = {16},
+ number = {3},
+ pages = {363--366},
+ issn = {1512-2891},
+ doi = {10.1007/s40062-021-00284-6},
+ abstract = {We show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $\infty$-groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky’s univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $\infty$-topos.},
+ langid = {english},
+ keywords = {55U40 03B15,Mathematics - Algebraic Geometry,Mathematics - Logic}
+}
+
+@online{Felixwellen/DCHoTT-Agda,
+ title = {Felixwellen/{{DCHoTT-Agda}}},
+ author = {Cherubini, Felix},
+ date = {2023-08-15T18:08:37Z},
+ origdate = {2016-09-12T17:09:29Z},
+ url = {https://github.com/felixwellen/DCHoTT-Agda},
+ abstract = {Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality},
+ howpublished = {{{GitHub}} repository}
+}
+
+@online{GGMS24,
+ title = {The {{Category}} of {{Iterative Sets}} in {{Homotopy Type Theory}} and {{Univalent Foundations}}},
+ author = {Gratzer, Daniel and Gylterud, Håkon and Mörtberg, Anders and Stenholm, Elisabeth},
+ date = {2024-02-07},
+ year = {2024},
+ month = {02},
+ eprint = {2402.04893},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ abstract = {When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. In this work, we equip the type of iterative sets V0, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V0 into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V0 and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V0 into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in Agda using the agda-unimath library of univalent mathematics.},
+ pubstate = {preprint},
+ keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic}
+}
+
+@inproceedings{JKFC23,
+ title = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}},
+ booktitle = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
+ author = {{{de}} Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie},
+ citeas = {JKFC23},
+ date = {2023-06-26},
+ year = {2023},
+ month = {06},
+ eprint = {2301.10696},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ pages = {1--13},
+ doi = {10.1109/LICS56636.2023.10175762},
+ abstract = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.},
+ keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic}
+}
+
+@book{May12,
+ title = {More {{Concise Algebraic Topology}}: {{Localization}}, {{Completion}}, and {{Model Categories}}},
+ shorttitle = {More {{Concise Algebraic Topology}}},
+ author = {May, J. P. and Ponto, K.},
+ date = {2012-02},
+ year = {2012},
+ month = {02},
+ publisher = {University of Chicago Press},
+ abstract = {With firm foundations dating only from the 1950s, algebraic topology is a relatively young area of mathematics. There are very few textbooks that treat fundamental topics beyond a first course, and many topics now essential to the field are not treated in any textbook. J. Peter May’s A Concise Course in Algebraic Topology addresses the standard first course material, such as fundamental groups, covering spaces, the basics of homotopy theory, and homology and cohomology. In this sequel, May and his coauthor, Kathleen Ponto, cover topics that are essential for algebraic topologists and others interested in algebraic topology, but that are not treated in standard texts. They focus on the localization and completion of topological spaces, model categories, and Hopf algebras. The first half of the book sets out the basic theory of localization and completion of nilpotent spaces, using the most elementary treatment the authors know of. It makes no use of simplicial techniques or model categories, and it provides full details of other necessary preliminaries. With these topics as motivation, most of the second half of the book sets out the theory of model categories, which is the central organizing framework for homotopical algebra in general. Examples from topology and homological algebra are treated in parallel. A short last part develops the basic theory of bialgebras and Hopf algebras.},
+ isbn = {978-0-226-51178-8},
+ langid = {english},
+ pagetotal = {544},
+ keywords = {Mathematics / Algebra / Abstract,Mathematics / General,Mathematics / Topology}
+}
+
+@book{May99,
+ title = {A {{Concise Course}} in {{Algebraic Topology}}},
+ author = {May, J. P.},
+ date = {1999-09},
+ year = {1999},
+ month = {09},
+ publisher = {University of Chicago Press},
+ abstract = {Algebraic topology is a basic part of modern mathematics, and some knowledge of this area is indispensable for any advanced work relating to geometry, including topology itself, differential geometry, algebraic geometry, and Lie groups. This book provides a detailed treatment of algebraic topology both for teachers of the subject and for advanced graduate students in mathematics either specializing in this area or continuing on to other fields. J. Peter May's approach reflects the enormous internal developments within algebraic topology over the past several decades, most of which are largely unknown to mathematicians in other fields. But he also retains the classical presentations of various topics where appropriate. Most chapters end with problems that further explore and refine the concepts presented. The final four chapters provide sketches of substantial areas of algebraic topology that are normally omitted from introductory texts, and the book concludes with a list of suggested readings for those interested in delving further into the field.},
+ isbn = {978-0-226-51183-2},
+ langid = {english},
+ pagetotal = {262},
+ keywords = {Mathematics / General,Mathematics / Topology},
+ url = {https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf}
+}
+
+@article{McAl74,
+ title = {Groups, {{Semilattices}} and {{Inverse Semigroups}}},
+ author = {McAlister, D. B.},
+ year = {1974},
+ journal = {Transactions of the American Mathematical Society},
+ volume = {192},
+ eprint = {1996831},
+ eprinttype = {jstor},
+ pages = {227--244},
+ publisher = {American Mathematical Society},
+ issn = {0002-9947},
+ doi = {10.2307/1996831},
+ abstract = {An inverse semigroup S is called proper if the equations ea = e = e2 together imply a2 = a for each a, e ∈ S. In this paper a construction is given for a large class of proper inverse semigroups in terms of groups and partially ordered sets; the semigroups in this class are called P-semigroups. It is shown that every inverse semigroup divides a P-semigroup in the sense that it is the image, under an idempotent separating homomorphism, of a full subsemigroup of a P-semigroup. Explicit divisions of this type are given for ω-bisimple semigroups, proper bisimple inverse semigroups, semilattices of groups and Brandt semigroups.}
+}
+
+@article{Mil84,
+ title = {The {{Sullivan Conjecture}} on {{Maps}} from {{Classifying Spaces}}},
+ author = {Miller, Haynes},
+ year = {1984},
+ journal = {Annals of Mathematics},
+ volume = {120},
+ number = {1},
+ eprint = {2007071},
+ eprinttype = {jstor},
+ pages = {39--87},
+ publisher = {Annals of Mathematics},
+ issn = {0003-486X},
+ doi = {10.2307/2007071}
+}
+
+@article{MP87,
+ title = {Inverse Semigroups and Extensions of Groups by Semilattices},
+ author = {Margolis, S. W and Pin, J. E},
+ date = {1987-10-15},
+ year = {1987},
+ month = {10},
+ journal = {Journal of Algebra},
+ shortjournal = {Journal of Algebra},
+ volume = {110},
+ number = {2},
+ pages = {277--297},
+ issn = {0021-8693},
+ doi = {10.1016/0021-8693(87)90046-9}
+}
+
+@online{MR23,
+ title = {Delooping the Sign Homomorphism in Univalent Mathematics},
+ author = {Mangel, Éléonore and Rijke, Egbert},
+ date = {2023-01-24},
+ year = {2023},
+ month = {01},
+ eprint = {2301.10011},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ abstract = {In univalent mathematics there are at least two equivalent ways to present the category of groups. Groups presented in their usual algebraic form are called abstract groups, and groups presented as pointed connected $1$-types are called concrete groups. Since these two descriptions of the category of groups are equivalent, we find that every algebraic group corresponds uniquely to a concrete group -- its delooping -- and that each abstract group homomorphisms corresponds uniquely to a pointed map between concrete groups. The $n$-th abstract symmetric group $S_n$ of all bijections $[n]\simeq [n]$, for instance, corresponds to the concrete group of all $n$-element types. The sign homomorphism from $S_n$ to $S_2$ should therefore correspond to a pointed map from the type $BS_n$ of all $n$-element types to the type $BS_2$ of all $2$-element types. Making use of the univalence axiom, we characterize precisely when a pointed map $BS_n\to_\ast BS_2$ is a delooping of the sign homomorphism. Then we proceed to give several constructions of the delooping of the sign homomorphism. Notably, the construction following a method of Cartier can be given without reference to the sign homomorphism. Our results are formalized in the agda-unimath library.},
+ pubstate = {preprint},
+ keywords = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic}
+}
+
+@book{MRR88,
+ title = {A {{Course}} in {{Constructive Algebra}}},
+ author = {Mines, Ray and Richman, Fred and Ruitenburg, Wim},
+ editorb = {Ewing, J. and Gehring, F. W. and Halmos, P. R.},
+ editorbtype = {redactor},
+ year = {1988},
+ series = {Universitext},
+ publisher = {Springer New York},
+ location = {New York, NY},
+ doi = {10.1007/978-1-4419-8640-5},
+ url = {http://link.springer.com/10.1007/978-1-4419-8640-5},
+ isbn = {978-0-387-96640-3 978-1-4419-8640-5}
+}
+
+@online{OEIS,
+ title = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})},
+ organization = {{{OEIS}} Foundation Inc.},
+ url = {https://oeis.org/}
+}
+
+@book{Rie17,
+ title = {Category {{Theory}} in {{Context}}},
+ author = {Riehl, Emily},
+ date = {2017-03-09},
+ year = {2017},
+ month = {03},
+ publisher = {Courier Dover Publications},
+ url = {https://math.jhu.edu/~eriehl/context.pdf},
+ abstract = {"The book is extremely pleasant to read, with masterfully crafted exercises and examples that create a beautiful and unique thread of presentation leading the reader safely into the wonderfully rich, expressive, and powerful theory of categories." — The Math Association Category theory has provided the foundations for many of the twentieth century's greatest advances in pure mathematics. This concise, original text for a one-semester course on the subject is derived from courses that author Emily Riehl taught at Harvard and Johns Hopkins Universities. The treatment introduces the essential concepts of category theory: categories, functors, natural transformations, the Yoneda lemma, limits and colimits, adjunctions, monads, and other topics. Suitable for advanced undergraduates and graduate students in mathematics, the text provides tools for understanding and attacking difficult problems in algebra, number theory, algebraic geometry, and algebraic topology. Drawing upon a broad range of mathematical examples from the categorical perspective, the author illustrates how the concepts and constructions of category theory arise from and illuminate more basic mathematical ideas. Prerequisites are limited to familiarity with some basic set theory and logic.},
+ isbn = {978-0-486-82080-4},
+ langid = {english},
+ pagetotal = {273},
+ keywords = {Mathematics / Logic}
+}
+
+@book{Rie22,
+ title = {Elements of $\infty$-{{Category Theory}}},
+ author = {Riehl, Emily and Verity, Dominic},
+ year = {2022},
+ series = {Cambridge {{Studies}} in {{Advanced Mathematics}}},
+ publisher = {Cambridge University Press},
+ location = {Cambridge},
+ doi = {10.1017/9781108936880},
+ url = {https://math.jhu.edu/~eriehl/elements.pdf},
+ abstract = {The language of $\infty$-categories provides an insightful new way of expressing many results in higher-dimensional mathematics but can be challenging for the uninitiated. To explain what exactly an $\infty$-category is requires various technical models, raising the question of how they might be compared. To overcome this, a model-independent approach is desired, so that theorems proven with any model would apply to them all. This text develops the theory of $\infty$-categories from first principles in a model-independent fashion using the axiomatic framework of an $\infty$-cosmos, the universe in which $\infty$-categories live as objects. An $\infty$-cosmos is a fertile setting for the formal category theory of $\infty$-categories, and in this way the foundational proofs in $\infty$-category theory closely resemble the classical foundations of ordinary category theory. Equipped with exercises and appendices with background material, this first introduction is meant for students and researchers who have a strong foundation in classical 1-category theory.},
+ isbn = {978-1-108-83798-9}
+}
+
+@online{Rij17,
+ title = {The Join Construction},
+ author = {Rijke, Egbert},
+ date = {2017-01-25},
+ year = {2017},
+ month = {01},
+ eprint = {1701.07538},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ urldate = {2023-02-05},
+ abstract = {In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-L\"of type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.},
+ pubstate = {preprint},
+ keywords = {Mathematics - Category Theory,Mathematics - Logic}
+}
+
+@phdthesis{Rij19,
+ title = {Classifying {{Types}}},
+ author = {Rijke, Egbert},
+ date = {2019-06-22},
+ year = {2019},
+ month = {06},
+ eprint = {1906.09435},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ abstract = {The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.},
+ pubstate = {preprint},
+ keywords = {Mathematics - Logic},
+ school = {Carnegie Mellon University}
+}
+
+@book{Rij22,
+ title = {Introduction to {{Homotopy Type Theory}}},
+ author = {Rijke, Egbert},
+ date = {2022-12-21},
+ year = {2022},
+ month = {12},
+ eprint = {2212.11082},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ abstract = {This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-L\"of's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.},
+ langid = {english},
+ publisher = {}
+}
+
+@online{Rij22draft,
+ title = {Introduction to {{Homotopy Type Theory}}},
+ author = {Rijke, Egbert},
+ year = {2022},
+ url = {https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf},
+ pubstate = {draft}
+}
+
+@article{RSS20,
+ title = {Modalities in Homotopy Type Theory},
+ author = {Rijke, Egbert and Shulman, Michael and Spitters, Bas},
+ date = {2020-01-08},
+ year = {2020},
+ month = {01},
+ eprint = {1706.07526},
+ eprinttype = {arxiv},
+ eprintclass = {cs, math},
+ journal = {Logical Methods in Computer Science},
+ volume = {Volume 16, Issue 1},
+ publisher = {Episciences.org},
+ issn = {1860-5974},
+ doi = {10.23638/LMCS-16(1:2)2020},
+ url = {https://lmcs.episciences.org/6015},
+ abstract = {Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.},
+ keywords = {Computer Science - Logic in Computer Science,F.3.1,F.3.1 F.4.1,F.4.1,Mathematics - Category Theory,Mathematics - Logic}
+}
+
+@inproceedings{SDR20,
+ title = {Sequential {{Colimits}} in {{Homotopy Type Theory}}},
+ booktitle = {Proceedings of the 35th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
+ author = {Sojakova, Kristina and {{van}} Doorn, Floris and Rijke, Egbert},
+ citeas = {SDR20},
+ date = {2020-07-08},
+ year = {2020},
+ month = {07},
+ series = {{{LICS}} '20},
+ pages = {845--858},
+ publisher = {Association for Computing Machinery},
+ location = {New York, NY, USA},
+ doi = {10.1145/3373718.3394801},
+ abstract = {Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.},
+ isbn = {978-1-4503-7104-9},
+ keywords = {higher inductive types,homotopy type theory,sequential colimits}
+}
+
+@online{Shu14SplittingIdempotents,
+ title = {Splitting {{Idempotents}}},
+ author = {Shulman, Mike},
+ date = {2014-12-08T07:44:32+00:00},
+ year = {2014},
+ month = {12},
+ url = {https://homotopytypetheory.org/2014/12/08/splitting-idempotents/},
+ abstract = {A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.},
+ langid = {english},
+ organization = {Homotopy Type Theory},
+ howpublished = {Blog post}
+}
+
+@online{Shu14UniversalProperties,
+ title = {Universal Properties without Function Extensionality},
+ author = {Shulman, Mike},
+ date = {2014-11-02T04:55:50+00:00},
+ year = {2014},
+ month = {11},
+ url = {https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/},
+ abstract = {A universal property, in the sense of category theory, generally expresses that a map involving hom-sets, induced by composition with some canonical map(s), is an isomorphism. In type theory we exp…},
+ langid = {english},
+ organization = {Homotopy Type Theory},
+ howpublished = {Blog post}
+}
+
+@article{Shu17,
+ title = {Idempotents in Intensional Type Theory},
+ author = {Shulman, Michael},
+ date = {2017-04-27},
+ year = {2017},
+ month = {04},
+ journal = {Logical Methods in Computer Science},
+ volume = {Volume 12, Issue 3},
+ publisher = {Episciences.org},
+ issn = {1860-5974},
+ doi = {10.2168/LMCS-12(3:9)2016},
+ url = {https://lmcs.episciences.org/2027},
+ abstract = {We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.}
+}
+
+@article{Shu18,
+ title = {Brouwer's Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory},
+ author = {Shulman, Michael},
+ date = {2018-06},
+ year = {2018},
+ month = {06},
+ eprint = {1509.07584},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ journal = {Mathematical Structures in Computer Science},
+ volume = {28},
+ number = {6},
+ pages = {856--941},
+ issn = {0960-1295, 1469-8072},
+ doi = {10.1017/S0960129517000147},
+ abstract = {We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental $\infty$-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.},
+ langid = {english},
+ keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic}
+}
+
+@book{SymmetryBook,
+ title = {Symmetry},
+ author = {Bezem, Marc and Buchholtz, Ulrik and Cagne, Pierre and Dundas, Bjørn Ian and Grayson, Daniel R},
+ date = {2023-06-07},
+ year = {2023},
+ month = {06},
+ url = {https://unimath.github.io/SymmetryBook/book.pdf},
+ langid = {english},
+ publisher = {}
+}
+
+@online{TypeTopology,
+ title = {{TypeTopology}},
+ author = {Escardó, Martín Hötzel and {contributors}},
+ citeas = {Esc},
+ url = {https://github.com/martinescardo/TypeTopology},
+ note = {{{Agda}} development},
+ howpublished = {{{GitHub}} repository}
+}
+
+@book{UF13,
+ title = {Homotopy {{Type Theory}}: {{Univalent Foundations}} of {{Mathematics}}},
+ shorttitle = {Homotopy {{Type Theory}}},
+ author = {{The Univalent Foundations Program}},
+ year = {2013},
+ eprint = {1308.0729},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ address = {Institute for Advanced Study},
+ url = {https://homotopytypetheory.org/book/},
+ langid = {english},
+ citeas = {UF13},
+ publisher = {}
+}
+
+@article{Voe10,
+ title = {Unstable Motivic Homotopy Categories in {{Nisnevich}} and Cdh-Topologies},
+ author = {Voevodsky, Vladimir},
+ date = {2010-08-01},
+ year = {2010},
+ month = {08},
+ eprint = {0805.4576},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ journal = {Journal of Pure and Applied Algebra},
+ shortjournal = {Journal of Pure and Applied Algebra},
+ volume = {214},
+ number = {8},
+ pages = {1399--1406},
+ issn = {0022-4049},
+ doi = {10.1016/j.jpaa.2009.11.005},
+ url = {https://www.sciencedirect.com/science/article/pii/S0022404909002643},
+ abstract = {The motivic homotopy categories can be defined with respect to different topologies and different underlying categories of schemes. For a number of reasons (mainly because of the Gluing Theorem) the motivic homotopy category of smooth schemes with respect to the Nisnevich topology plays a distinguished role but in some cases it is desirable to be able to work with all schemes instead of the smooth ones. In this paper we prove that, under the resolution of singularities assumption, the unstable motivic homotopy category of all schemes over a field with respect to the cdh-topology is almost equivalent to the unstable motivic homotopy category of smooth schemes over the same field with respect to the Nisnevich topology.},
+ keywords = {14F42,Mathematics - Algebraic Geometry}
+}
+
+@misc{Warn23draft,
+ title = {Path Spaces of Pushouts},
+ author = {Wärn, David},
+ date = {4/21/2023, 12:04:00 AM},
+ year = {2023},
+ month = {04},
+ howpublished = {E-mail},
+ url = {https://dwarn.se/po-paths.pdf},
+ abstract = {Working in homotopy type theory, we describe path spaces of pushouts as sequential colimits of pushouts. This gives a higher Seifert–van Kampen theorem. We demonstrate the utility of this description by showing that any pushout of 0-types is a 1-type, settling a long-standing open question in homotopy type theory. Our construction can be interpreted in any higher category with pullbacks, finite colimits satisfying descent, and sequential colimits.},
+ langid = {english}
+}
+
+@online{Warn24,
+ title = {Path Spaces of Pushouts},
+ author = {Wärn, David},
+ date = {2024-02-19},
+ year = {2024},
+ month = {02},
+ eprint = {2402.12339},
+ eprinttype = {arxiv},
+ eprintclass = {math},
+ urldate = {2024-02-26},
+ abstract = {Given a span of spaces, one can form the homotopy pushout and then take the homotopy pullback of the resulting cospan. We give a concrete description of this pullback as the colimit of a sequence of approximations, using what we call the zigzag construction. We also obtain a description of loop spaces of homotopy pushouts. Using the zigzag construction, we reproduce generalisations of the Blakers-Massey theorem and fundamental results from Bass-Serre theory. We also describe the loop space of a wedge and show that it splits after suspension. Our construction can be interpreted in a large class of $(\infty,1)$-categories and in homotopy type theory, where it resolves the long-standing open problem of showing that a pushout of 0-types is 1-truncated. The zigzag construction is closely related to the James construction, but works in greater generality.},
+ pubstate = {preprint},
+ keywords = {Mathematics - Algebraic Topology,Mathematics - Category Theory}
+}
diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py
index ac5ae4507d..abecb33c1b 100755
--- a/scripts/generate_main_index_file.py
+++ b/scripts/generate_main_index_file.py
@@ -109,6 +109,7 @@ def generate_index(root_path, header):
- [File template](TEMPLATE.lagda.md)
- [The library coding style](CODINGSTYLE.md)
- [Guidelines for mixfix operators](MIXFIX-OPERATORS.md)
+ - [Citing sources](CITING-SOURCES.md)
- [Citing the library](CITE-THIS-LIBRARY.md)
- [Library contents](SUMMARY.md)
- [Art](ART.md)
diff --git a/scripts/preprocessor_citations.py b/scripts/preprocessor_citations.py
new file mode 100644
index 0000000000..ea5a81b9ba
--- /dev/null
+++ b/scripts/preprocessor_citations.py
@@ -0,0 +1,265 @@
+#!/usr/bin/env python3
+
+# This file is intended to be used as a mdbook preprocessor,
+# and it adheres to the appropriate protocol; see
+# https://rust-lang.github.io/mdBook/for_developers/preprocessors.html#hooking-into-mdbook
+
+import re
+import pybtex
+import pybtex.database
+import pybtex.plugin
+import pybtex.backends
+import pybtex.backends.html
+import pybtex.style.formatting
+import pybtex.style.formatting.alpha
+import pybtex.style.labels.alpha
+import sys
+import io
+from utils import eprint
+import json
+
+# Defaults and other constants
+CITEAS_FIELD = 'citeas'
+DEFAULT_CITATION_STYLE = 'alpha'
+DEFAULT_LABEL_CITATION_STYLE = 'custom_alpha'
+DEFAULT_ERROR_ON_UNMATCHED_CITE_KEY = True
+
+# Regex to match citation macros
+CITE_REGEX = re.compile(r'\{\{#cite\s([^\}\s]+)(?:\s(.*))?\}\}')
+# NO_REF_CITE_REGEX = re.compile(r'(?\n')
+
+ def write_epilogue(self):
+ self.output('\n\n')
+
+ def write_entry(self, key, label, text):
+ self.output(f'[{label}]\n')
+ self.output(f'{text}\n')
+
+
+class CustomAlphaLabelStyle(pybtex.style.labels.alpha.LabelStyle):
+ """
+ Custom pybtex plugin for the alpha label style which overwrites it with the
+ contents of the 'citeas' field of a bibliography entry if present.
+ """
+
+ def format_label(self, entry):
+ if CITEAS_FIELD in entry.fields.keys():
+ return entry.fields[CITEAS_FIELD]
+ else:
+ return super().format_label(entry)
+
+
+# Register custom pybtex plugins
+pybtex.plugin.register_plugin(
+ 'pybtex.backends', 'custom_html', CustomHtmlBackend)
+pybtex.plugin.register_plugin(
+ 'pybtex.style.labels', 'custom_alpha', CustomAlphaLabelStyle)
+
+
+def render_references(
+ bib_database: pybtex.database.BibliographyData,
+ style: pybtex.style.formatting.BaseStyle,
+ backend: pybtex.backends.BaseBackend,
+ cited_keys):
+ formatted_bibliography = style.format_bibliography(
+ bib_database, tuple(cited_keys))
+
+ output = io.StringIO()
+ backend.write_to_stream(formatted_bibliography, output)
+ html = output.getvalue()
+
+ return html
+
+
+def format_citation(
+ bib_database: pybtex.database.BibliographyData,
+ style: pybtex.style.formatting.BaseStyle,
+ match,
+ cited_keys: set,
+ unmatched_cite_keys: set,
+ chapter):
+ cite_key = match.group(1)
+
+ # Function to format the citation and collect cited keys
+ if cite_key in bib_database.entries:
+ # if not match.group(2) or not NO_REF_CITE_REGEX.search(match.group(2)):
+ cited_keys.add(cite_key)
+
+ cite_entry = bib_database.entries[cite_key]
+
+ formatted_label = style.label_style.format_label(cite_entry)
+
+ return f'[{formatted_label}]'
+ else:
+ eprint(f"Error! Citation key '{cite_key}' used in #cite macro was not found in bibliography. File: '{chapter['path']}'")
+ unmatched_cite_keys.add(cite_key)
+ # If the cite_key is not recognized, we make the following guess about how to format the citation instead of failing completely
+ return f'[{cite_key}]'
+
+
+def generate_bibliography(
+ bib_database: pybtex.database.BibliographyData,
+ style: pybtex.style.formatting.BaseStyle,
+ backend: pybtex.backends.BaseBackend,
+ cited_keys):
+ # Function to generate the bibliography section
+ return render_references(bib_database, style, backend, cited_keys)
+
+
+def process_citations_chapter_rec_mut(
+ chapter,
+ bib_database: pybtex.database.BibliographyData,
+ style: pybtex.style.formatting.BaseStyle,
+ backend,
+ unmatched_cite_keys: set):
+ cited_keys = set() # Set to keep track of all cited keys
+ content = chapter.get('content', '')
+ new_content = CITE_REGEX.sub(lambda match: format_citation(
+ bib_database, style, match, cited_keys, unmatched_cite_keys, chapter) or match.group(0), content)
+
+ def sub_reference_regex_lambda(m):
+ cite_key = m.group(1)
+ if cite_key in bib_database.entries:
+ cited_keys.add(cite_key)
+ return ''
+ else:
+ eprint(f"Error! Citation key '{cite_key}' used in #reference macro was not found in bibliography. File: '{chapter['path']}'")
+ unmatched_cite_keys.add(cite_key)
+ return ''
+
+ new_content = REFERENCE_REGEX.sub(sub_reference_regex_lambda, new_content)
+
+ if cited_keys:
+ bibliography_section = generate_bibliography(
+ bib_database, style, backend, cited_keys)
+ if bibliography_section:
+ new_content = insert_bibliography_at_correct_location(
+ new_content, bibliography_section)
+
+ chapter['content'] = new_content
+
+ process_citations_sections_rec_mut(
+ chapter['sub_items'], bib_database, style, backend, unmatched_cite_keys)
+
+
+def insert_bibliography_at_correct_location(content, bibliography_section):
+
+ # Search for the placeholder in the content
+ match = BIBLIOGRAPHY_REGEX.search(content)
+
+ if match:
+ # Replace the placeholder with the bibliography section
+ new_content = BIBLIOGRAPHY_REGEX.sub(
+ lambda _: bibliography_section, content)
+ else:
+ # If the placeholder isn't found, append the bibliography at the end of the content, with a `## References` header
+ new_content = content + "\n\n## References\n\n" + bibliography_section
+
+ return new_content
+
+
+def process_citations_sections_rec_mut(
+ sections,
+ bib_database,
+ style: pybtex.style.formatting.BaseStyle,
+ backend: pybtex.backends.BaseBackend,
+ unmatched_cite_keys: set):
+ for section in sections:
+ chapter = section.get('Chapter')
+ if chapter is None:
+ continue
+
+ process_citations_chapter_rec_mut(
+ chapter, bib_database, style, backend, unmatched_cite_keys)
+
+
+def process_citations_root_section(
+ section,
+ bib_database: pybtex.database.BibliographyData,
+ style: pybtex.style.formatting.BaseStyle,
+ backend: pybtex.backends.BaseBackend,
+ unmatched_cite_keys: set):
+ chapter = section.get('Chapter')
+ if chapter is not None:
+ process_citations_chapter_rec_mut(
+ chapter, bib_database, style, backend, unmatched_cite_keys)
+
+ return section
+
+
+def does_support_backend(backend):
+ return backend == 'html' or backend == "linkcheck"
+
+
+if __name__ == '__main__':
+ if len(sys.argv) > 1:
+ arguments = sys.argv[1:]
+ if arguments[0] == 'supports':
+ backend = arguments[1]
+ if does_support_backend(backend):
+ sys.exit(0)
+ else:
+ sys.exit(1)
+
+ context, book = json.load(sys.stdin)
+ citations_config = context['config']['preprocessor']['citations']
+
+ unmatched_cite_keys = set()
+
+ if bool(citations_config.get('enable', True)):
+ bib_database: pybtex.database.BibliographyData = pybtex.database.parse_file(
+ citations_config.get('bibtex_file'))
+
+ # Config
+ citation_style_config = citations_config.get(
+ 'citation_style', DEFAULT_CITATION_STYLE)
+ label_style_config = citations_config.get(
+ 'citation_label_style', DEFAULT_LABEL_CITATION_STYLE)
+ backend_config = 'custom_html'
+
+ # Initialize pybtex classes
+ style_class = pybtex.plugin.find_plugin(
+ 'pybtex.style.formatting', citation_style_config)
+ style: pybtex.style.formatting.BaseStyle = style_class(
+ label_style=pybtex.plugin.find_plugin('pybtex.style.labels', label_style_config))
+ backend: pybtex.backends.BaseBackend = pybtex.plugin.find_plugin(
+ 'pybtex.backends', backend_config)()
+
+ # The following must be run in order to detect errors and missing fields in the bibtex file
+ formatted_bibliography: pybtex.style.FormattedBibliography = \
+ style.format_bibliography(bib_database)
+ # # Optional: print to error stream
+ # output = io.StringIO()
+ # backend.write_to_stream(formatted_bibliography, output)
+ # html = output.getvalue()
+ # eprint(html)
+
+ book['sections'] = list(map(
+ lambda s: process_citations_root_section(
+ s, bib_database, style, backend, unmatched_cite_keys),
+ book['sections']))
+ else:
+ eprint('Skipping citation insertion, enable option was set to',
+ citations_config.get('enable'))
+
+ json.dump(book, sys.stdout)
+
+ if unmatched_cite_keys:
+ eprint("The following unmatched bibliography keys were found while processing citations: ", ", ".join(sorted(unmatched_cite_keys)))
+
+ if citations_config.get('error_on_unmatched_keys', DEFAULT_ERROR_ON_UNMATCHED_CITE_KEY):
+ sys.exit(1)
diff --git a/scripts/preprocessor_concepts.py b/scripts/preprocessor_concepts.py
index 98bd48074a..b37a6dba09 100644
--- a/scripts/preprocessor_concepts.py
+++ b/scripts/preprocessor_concepts.py
@@ -203,18 +203,14 @@ def tag_concepts_root_section(section, config, mut_index):
# Thread the index through execution
mut_index = []
- start = time.time()
if bool(concepts_config.get('enable', True)) == True:
book['sections'] = list(map(
lambda s: tag_concepts_root_section(s, concepts_config, mut_index),
book['sections']))
else:
- eprint('Skipping concept tagging, enable option was',
+ eprint('Skipping concept tagging, enable option was set to',
concepts_config.get('enable'))
- end = time.time()
- eprint(end - start)
-
if mut_index != []:
with open(concepts_config.get('output-file', 'concept_index.json'), 'w') as index_f:
json.dump(mut_index, index_f)
diff --git a/scripts/preprocessor_git_metadata.py b/scripts/preprocessor_git_metadata.py
index 2fd400a480..4ae55ce744 100644
--- a/scripts/preprocessor_git_metadata.py
+++ b/scripts/preprocessor_git_metadata.py
@@ -221,8 +221,7 @@ def add_author_info_to_root_section(roots, section, contributors, config):
metadata_config['suppress_processing'] = metadata_config.get(
'suppress_processing', [])
- start = time.time()
- if bool(metadata_config.get('enable')) == True:
+ if bool(metadata_config.get('enable')):
# Split the work between PROCESS_COUNT processes
with Pool(PROCESS_COUNT) as p:
book['sections'] = p.starmap(add_author_info_to_root_section, [
@@ -230,11 +229,8 @@ def add_author_info_to_root_section(roots, section, contributors, config):
for section in book['sections']
])
else:
- eprint('Skipping git metadata, enable option was',
+ eprint('Skipping git metadata, enable option was set to',
metadata_config.get('enable'))
- end = time.time()
- eprint(end - start)
-
# Pass the book back to mdbook
json.dump(book, sys.stdout)
diff --git a/scripts/requirements.txt b/scripts/requirements.txt
index d9c7e98901..16aa1abdb5 100644
--- a/scripts/requirements.txt
+++ b/scripts/requirements.txt
@@ -1,4 +1,5 @@
# * Keep in sync with the `flake.nix` file
pre-commit
+pybtex
requests
tomli
diff --git a/src/category-theory/essentially-surjective-functors-precategories.lagda.md b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
index 953f99f962..ef49c3c337 100644
--- a/src/category-theory/essentially-surjective-functors-precategories.lagda.md
+++ b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
@@ -114,10 +114,7 @@ Rezk completion_.
## References
-1. Benedikt Ahrens and Krzysztof Kapulkin and Michael Shulman, _Univalent
- Categories and the Rezk completion_ (2015)
- ([arXiv:1303.0584](https://arxiv.org/abs/1303.0584),
- [DOI:10.1017/S0960129514000486](https://doi.org/10.1017/S0960129514000486))
+{{#bibliography}} {{#reference AKS15}}
## External links
diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
index ca61deca29..6cd590ab79 100644
--- a/src/category-theory/functors-precategories.lagda.md
+++ b/src/category-theory/functors-precategories.lagda.md
@@ -532,13 +532,7 @@ module _
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
-2. Benedikt Ahrens and Krzysztof Kapulkin and Michael Shulman, _Univalent
- Categories and the Rezk completion_ (2015)
- ([arXiv:1303.0584](https://arxiv.org/abs/1303.0584),
- [DOI:10.1017/S0960129514000486](https://doi.org/10.1017/S0960129514000486))
+{{#bibliography}} {{#reference UF13}} {{#reference AKS15}}
## External links
diff --git a/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md b/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
index 37871d352f..2c369636ce 100644
--- a/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
+++ b/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
@@ -173,10 +173,7 @@ Rezk completion_.
## References
-1. Benedikt Ahrens and Krzysztof Kapulkin and Michael Shulman, _Univalent
- Categories and the Rezk completion_ (2015)
- ([arXiv:1303.0584](https://arxiv.org/abs/1303.0584),
- [DOI:10.1017/S0960129514000486](https://doi.org/10.1017/S0960129514000486))
+{{#bibliography}} {{#reference AKS15}}
## External links
diff --git a/src/elementary-number-theory/cofibonacci.lagda.md b/src/elementary-number-theory/cofibonacci.lagda.md
index 8307f2cec6..a5c3b562c0 100644
--- a/src/elementary-number-theory/cofibonacci.lagda.md
+++ b/src/elementary-number-theory/cofibonacci.lagda.md
@@ -139,6 +139,6 @@ is-left-adjoint-cofibonacci m n = {!!}
-}
```
-## References
+## External links
[1]: https://oeis.org/A001177
diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
index b9c9ba02b5..78b0a6dcbc 100644
--- a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
@@ -202,5 +202,4 @@ module _
## References
-- Mangel É. and Rijke E.
- ["Delooping the sign homomorphism in univalent mathematics"](https://arxiv.org/abs/2301.10011).
+{{#bibliography}} {{#reference MR23}}
diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
index e34a655ed0..3de1b68a34 100644
--- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
@@ -1598,5 +1598,4 @@ module _
## References
-- Mangel É. and Rijke E.
- ["Delooping the sign homomorphism in univalent mathematics"](https://arxiv.org/abs/2301.10011).
+{{#bibliography}} {{#reference MR23}}
diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
index f8941726e6..479553f8ba 100644
--- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
@@ -800,5 +800,4 @@ module _
## References
-- Mangel É. and Rijke E.
- ["Delooping the sign homomorphism in univalent mathematics"](https://arxiv.org/abs/2301.10011).
+{{#bibliography}} {{#reference MR23}}
diff --git a/src/foundation-core/coherently-invertible-maps.lagda.md b/src/foundation-core/coherently-invertible-maps.lagda.md
index 596c722080..59dffb154a 100644
--- a/src/foundation-core/coherently-invertible-maps.lagda.md
+++ b/src/foundation-core/coherently-invertible-maps.lagda.md
@@ -459,8 +459,7 @@ module _
This result is known as
[Vogt's lemma](https://ncatlab.org/nlab/show/homotopy+equivalence#vogts_lemma)
-in point-set topology. The construction follows Lemma 10.4.5 in _Introduction to
-Homotopy Type Theory_.
+in point-set topology. The construction follows Lemma 10.4.5 in {{#cite Rij22}}.
```agda
module _
@@ -624,8 +623,7 @@ module _
### Coherently invertible maps are transpose coherently invertible
-The proof follows Lemma 4.2.2 in _Homotopy Type Theory – Univalent Foundations
-of Mathematics_.
+The proof follows Lemma 4.2.2 in {{#cite UF13}}.
**Proof.** By naturality of homotopies we have
@@ -1387,11 +1385,7 @@ module _
## References
-1. Egbert Rijke, _Introduction to Homotopy Type Theory_ (2022)
- ([arXiv:2212.11082](https://arxiv.org/abs/2212.11082))
-2. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
+{{#bibliography}}
## See also
diff --git a/src/foundation-core/path-split-maps.lagda.md b/src/foundation-core/path-split-maps.lagda.md
index c2b94a4453..2d4e324279 100644
--- a/src/foundation-core/path-split-maps.lagda.md
+++ b/src/foundation-core/path-split-maps.lagda.md
@@ -88,9 +88,4 @@ module _
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
-2. Mike Shulman, _Universal properties without function extensionality_
- (November 2014)
- ([HoTT Blog](https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/))
+{{#bibliography}} {{#reference UF13}} {{#reference Shu14UniversalProperties}}
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index 94d5fe5e54..dcfdd594ff 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -530,7 +530,9 @@ over the pullbacks as in the following diagram
Then the pasting `γ □ α` is a pullback if and only if `γ` is if and only if the
pasting `γ □ β` is. And, in particular, we have the equivalence
-\[ (A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C). \]
+$$
+(A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C).
+$$
```agda
module _
diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
index 4419efd46b..70bdbea7f6 100644
--- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
+++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
@@ -30,11 +30,12 @@ open import foundation-core.negation
## Idea
The classical Cantor–Schröder–Bernstein theorem asserts that from any pair of
-injective maps `f : A → B` and `g : B → A` we can construct a bijection between
-`A` and `B`. In a recent generalization, Escardó proved that a
-Cantor–Schröder–Bernstein theorem also holds for ∞-groupoids. His generalization
-asserts that given two types that embed into each other, then the types are
-equivalent.
+[injective maps](foundation-core.injective-maps.md) `f : A → B` and `g : B → A`
+we can construct a bijection between `A` and `B`. In a recent generalization,
+Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
+∞-groupoids. His generalization asserts that given two types that
+[embed](foundation-core.embeddings.md) into each other, then the types are
+[equivalent](foundation-core.equivalences.md). {{#cite Esc21}}
## Statement
@@ -173,8 +174,8 @@ module _
## References
-- Martín H. Escardó, _The Cantor–Schröder–Bernstein Theorem for ∞-groupoids_,
- Journal of Homotopy and Related Structures, Volume 16, Issue 3, 2021
- ([arXiv:2002.07079](https://arxiv.org/abs/2002.07079),[DOI:10.1007/S40062-021-00284-6](https://doi.org/10.1007/s40062-021-00284-6))
- -
- -
+- Escardó's formalizations regarding this theorem can be found at
+ .
+ {{#cite TypeTopology}}
+
+{{#bibliography}}
diff --git a/src/foundation/coherently-invertible-maps.lagda.md b/src/foundation/coherently-invertible-maps.lagda.md
index d43a5f5702..4a590a17f1 100644
--- a/src/foundation/coherently-invertible-maps.lagda.md
+++ b/src/foundation/coherently-invertible-maps.lagda.md
@@ -123,9 +123,7 @@ This remains to be formalized.
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
+{{#bibliography}} {{#reference UF13}}
## See also
diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md
index 6bc5ca1be2..1e406c460d 100644
--- a/src/foundation/double-negation-modality.lagda.md
+++ b/src/foundation/double-negation-modality.lagda.md
@@ -63,11 +63,8 @@ is-uniquely-eliminating-modality-double-negation-modality {l} {A} P =
( z))
```
-This proof follows Example 1.9 in _Modalities in homotopy type theory_.
+This proof follows Example 1.9 in {{#cite RSS20}}.
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}}
diff --git a/src/foundation/locally-small-types.lagda.md b/src/foundation/locally-small-types.lagda.md
index bbebd0d8db..3d7842ecda 100644
--- a/src/foundation/locally-small-types.lagda.md
+++ b/src/foundation/locally-small-types.lagda.md
@@ -277,9 +277,7 @@ is-locally-small-inhabited-subtype H =
## References
-- Egbert Rijke, Theorem 4.6 in _The join construction_, 2017
- ([arXiv:1701.07538](https://arxiv.org/abs/1701.07538))
-- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R.
- Grayson, Section 2.19 of _Symmetry_
- ([draft](https://unimath.github.io/SymmetryBook/book.pdf),
- [GitHub](https://github.com/UniMath/SymmetryBook))
+- Theorem 4.6 in {{#cite Rij17}}.
+- Section 2.19 in {{#cite SymmetryBook}}.
+
+{{#bibliography}}
diff --git a/src/foundation/path-split-maps.lagda.md b/src/foundation/path-split-maps.lagda.md
index 2a4f022646..857a1071b5 100644
--- a/src/foundation/path-split-maps.lagda.md
+++ b/src/foundation/path-split-maps.lagda.md
@@ -82,9 +82,4 @@ module _
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
-2. Mike Shulman, _Universal properties without function extensionality_
- (November 2014)
- ([HoTT Blog](https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/))
+{{#bibliography}} {{#reference UF13}} {{#reference Shu14UniversalProperties}}
diff --git a/src/foundation/preidempotent-maps.lagda.md b/src/foundation/preidempotent-maps.lagda.md
index 0e3a918a15..90324eb1de 100644
--- a/src/foundation/preidempotent-maps.lagda.md
+++ b/src/foundation/preidempotent-maps.lagda.md
@@ -46,8 +46,4 @@ is-prop-is-preidempotent-is-set is-set-A f =
## References
-- Mike Shulman, _Idempotents in intensional type theory_, Logical Methods in
- Computer Science, Volume 12, Issue 3, 2017
- ([arXiv:1507.03634](https://arxiv.org/abs/1507.03634))
-- Mike Shulman, _Splitting Idempotents_,
-
+{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}}
diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
index f9f9830a30..6c408e63e6 100644
--- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
+++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -254,8 +254,9 @@ files:
## References
-- Two special cases of the extended fundamental theorem of identity types are
- stated in the Introduction to Homotopy Type Theory textbook by Egbert Rijke:
- The case where `P` is the subuniverse of `k`-truncated types is stated as
- Theorem 19.6.2; and the case where `P` is the subuniverse of inhabited types
- is stated as Exercise 19.14.
+Two special cases of the extended fundamental theorem of identity types are
+stated in {{#cite Rij22}}: The case where `P` is the subuniverse of
+`k`-truncated types is stated as Theorem 19.6.2; and the case where `P` is the
+subuniverse of inhabited types is stated as Exercise 19.14.
+
+{{#bibliography}}
diff --git a/src/foundation/replacement.lagda.md b/src/foundation/replacement.lagda.md
index 0104411031..f399430bcb 100644
--- a/src/foundation/replacement.lagda.md
+++ b/src/foundation/replacement.lagda.md
@@ -56,9 +56,7 @@ replacement' f = replacement f is-small'
## References
-- Egbert Rijke, Theorem 4.6 in _The join construction_, 2017
- ([arXiv:1701.07538](https://arxiv.org/abs/1701.07538))
-- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R.
- Grayson, Section 2.19 of _Symmetry_
- ([newest version](https://unimath.github.io/SymmetryBook/book.pdf),
- [GitHub](https://github.com/UniMath/SymmetryBook))
+- Theorem 4.6 in {{#cite Rij17}}.
+- Section 2.19 in {{#cite SymmetryBook}}.
+
+{{#bibliography}}
diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md
index f9cf20e78a..aef92b7348 100644
--- a/src/foundation/retracts-of-maps.lagda.md
+++ b/src/foundation/retracts-of-maps.lagda.md
@@ -908,10 +908,7 @@ module _
## References
-1. Section 4.7 of Univalent Foundations Project, _Homotopy Type Theory –
- Univalent Foundations of Mathematics_ (2013)
- ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
+{{#bibliography}} {{#reference UF13}}
## External links
diff --git a/src/foundation/strictly-involutive-identity-types.lagda.md b/src/foundation/strictly-involutive-identity-types.lagda.md
index 79e477f008..78402e0de3 100644
--- a/src/foundation/strictly-involutive-identity-types.lagda.md
+++ b/src/foundation/strictly-involutive-identity-types.lagda.md
@@ -733,4 +733,4 @@ module _
## References
--
+{{#bibliography}} {{#reference Esc19DefinitionsEquivalence}}
diff --git a/src/foundation/truncation-equivalences.lagda.md b/src/foundation/truncation-equivalences.lagda.md
index b33ed89007..e32a7406dc 100644
--- a/src/foundation/truncation-equivalences.lagda.md
+++ b/src/foundation/truncation-equivalences.lagda.md
@@ -262,8 +262,7 @@ module _
### The map on dependent pair types induced by the unit of the `(k+1)`-truncation is a `k`-equivalence
-This is an instance of Lemma 2.27 in Christensen, Opie, Rijke & Scoccola
-\[CORS'20\] listed below.
+This is an instance of Lemma 2.27 in {{#cite CORS20}} listed below.
```agda
module _
@@ -295,7 +294,7 @@ module _
### There is an `k`-equivalence between the fiber of a map and the fiber of its `(k+1)`-truncation
-This is an instance of Corollary 2.29 in \[CORS'20\].
+This is an instance of Corollary 2.29 in {{#cite CORS20}}.
We consider the following composition of maps
@@ -381,7 +380,7 @@ module _
### Every `(k+1)`-equivalence is `k`-connected
-This is an instance of Proposition 2.30 in \[CORS'20\].
+This is an instance of Proposition 2.30 in {{#cite CORS20}}.
```agda
module _
@@ -398,7 +397,7 @@ module _
### The codomain of a `k`-connected map is `(k+1)`-connected if its domain is `(k+1)`-connected
-This follows part of the proof of Proposition 2.31 in \[CORS'20\].
+This follows part of the proof of Proposition 2.31 in {{#cite CORS20}}.
```agda
module _
@@ -449,7 +448,7 @@ module _
### If `g ∘ f` is `(k+1)`-connected, then `f` is `k`-connected if and only if `g` is `(k+1)`-connected
-This is an instance of Proposition 2.31 in \[CORS'20\].
+This is an instance of Proposition 2.31 in {{#cite CORS20}}.
```agda
module _
@@ -502,15 +501,10 @@ module _
## References
-The notion of `k`-equivalence is a special case of the notion of
-`L`-equivalence, where `L` is a reflective subuniverse. They were studied in the
-paper
+- The notion of `k`-equivalence is a special case of the notion of
+ `L`-equivalence, where `L` is a reflective subuniverse. They were studied in
+ the paper {{#cite CORS20}}.
+- The class of `k`-equivalences is left orthogonal to the class of `k`-étale
+ maps. This was shown in {{#cite CR21}}.
-- \[CORS'20\]: J. D. Christensen, M. Opie, E. Rijke, and L. Scoccola.
- Localization in Homotopy Type Theory. Higher Structures, 2020.
-
-The class of `k`-equivalences is left orthogonal to the class of `k`-étale maps.
-This was shown in
-
-- \[CR'21\]: F. Cherubini, and E. Rijke. Modal descent. Mathematical Structures
- in Computer Science, 2021.
+{{#bibliography}}
diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md
index ff221ee45b..e2ff4ee524 100644
--- a/src/foundation/universal-property-cartesian-product-types.lagda.md
+++ b/src/foundation/universal-property-cartesian-product-types.lagda.md
@@ -44,12 +44,16 @@ Observe that the universal property of cartesian products as limits can be
understood as a categorified version of the familiar distributivity of exponents
over products
-\[ (A × B)^X ≃ A^X × B^X, \]
+$$
+(A × B)^X ≃ A^X × B^X,
+$$
while the universal property of cartesian products as colimits are a
categorified version of the identity
-\[ X^{(A × B)} ≃ {(X^B)}^A. \]
+$$
+X^{(A × B)} ≃ {(X^B)}^A.
+$$
## Theorems
diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index 1707d38d81..e3ec6f2c01 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/src/foundation/universal-property-identity-types.lagda.md
@@ -223,3 +223,5 @@ module _
`Id : A → (A → 𝒰)` is an embedding was first observed and formalized by Martín
Escardó,
[https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html](https://www.cs.bham.ac.uk//~mhe/TypeTopology/UF.IdEmbedding.html).
+
+{{#bibliography}} {{#reference TypeTopology}}
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index c763b6c36a..9e873169c8 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -945,4 +945,4 @@ module _
## References
--
+{{#bibliography}} {{#reference Esc19DefinitionsEquivalence}}
diff --git a/src/group-theory/cayleys-theorem.lagda.md b/src/group-theory/cayleys-theorem.lagda.md
index 817b6227e0..8a1459ba57 100644
--- a/src/group-theory/cayleys-theorem.lagda.md
+++ b/src/group-theory/cayleys-theorem.lagda.md
@@ -63,13 +63,11 @@ module _
### Cayley's theorem as a corollary of the Yoneda lemma
-This is Corollary 2.2.10 of _Category theory in context_, and remains to be
-formalized.
+This is Corollary 2.2.10 of {{#cite Rie17}}, and remains to be formalized.
## References
-1. Emily Riehl, _Category Theory in Context_, 2016
- ([PDF](https://math.jhu.edu/~eriehl/context.pdf))
+{{#bibliography}}
## External links
diff --git a/src/group-theory/normal-submonoids.lagda.md b/src/group-theory/normal-submonoids.lagda.md
index 982c97e4b8..45aaa58a2c 100644
--- a/src/group-theory/normal-submonoids.lagda.md
+++ b/src/group-theory/normal-submonoids.lagda.md
@@ -576,5 +576,4 @@ pr2 (equiv-normal-submonoid-saturated-congruence-Monoid l2 M) =
## References
-- S. Margolis and J.-É. Pin, Inverse semigroups and extensions of groups by
- semilattices, J. of Algebra 110 (1987), 277-297.
+{{#bibliography}} {{#reference MP87}}
diff --git a/src/higher-group-theory/cyclic-higher-groups.lagda.md b/src/higher-group-theory/cyclic-higher-groups.lagda.md
index d0c2493c1c..34d954d1f2 100644
--- a/src/higher-group-theory/cyclic-higher-groups.lagda.md
+++ b/src/higher-group-theory/cyclic-higher-groups.lagda.md
@@ -36,13 +36,13 @@ given by `f ↦ map-hom-∞-Group G H f g` is an
[embedding](foundation.embeddings.md) for every higher group `H`. In other
words, a higher group is cyclic if it is generated by a single element.
-However, by Miller's theorem we don't expect there to be many higher groups that
-are cyclic in this sense. For example, the finite cyclic groups `Bℤ/n` are
-coherent spaces, whereas the 2-sphere `S²` is a finite CW-complex. Miller's
-theorem implies that the pointed mapping space `Map∗(Bℤ/n,S²)` is contractible.
-However, this implies that the evaluation map `Map∗(Bℤ/n,S²) → ΩS²` at the
-generator of `ℤ/n` is a point inclusion into a nondiscrete type, so it can't be
-an embedding.
+However, by Miller's theorem {{#cite Mil84}} we don't expect there to be many
+higher groups that are cyclic in this sense. For example, the finite cyclic
+groups `Bℤ/n` are coherent spaces, whereas the 2-sphere `S²` is a finite
+CW-complex. Miller's theorem implies that the pointed mapping space
+`Map∗(Bℤ/n,S²)` is contractible. However, this implies that the evaluation map
+`Map∗(Bℤ/n,S²) → ΩS²` at the generator of `ℤ/n` is a point inclusion into a
+nondiscrete type, so it can't be an embedding.
## Definitions
@@ -79,6 +79,4 @@ module _
## References
-1. Haynes Miller. _The Sullivan Conjecture on Maps from Classifying Spaces_.
- Annals of Mathematics 120.1 (1984), pp. 39–87. issn: 0003486X.
-
+{{#bibliography}}
diff --git a/src/modal-type-theory/flat-dependent-function-types.lagda.md b/src/modal-type-theory/flat-dependent-function-types.lagda.md
index 9d7127b515..45cdb77663 100644
--- a/src/modal-type-theory/flat-dependent-function-types.lagda.md
+++ b/src/modal-type-theory/flat-dependent-function-types.lagda.md
@@ -53,7 +53,4 @@ module _
## References
-- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type
- theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584))
-- Dan Licata, _cohesion-agda_, GitHub repository
- ()
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-dependent-pair-types.lagda.md b/src/modal-type-theory/flat-dependent-pair-types.lagda.md
index 3e6cf4e8dc..b59f618c57 100644
--- a/src/modal-type-theory/flat-dependent-pair-types.lagda.md
+++ b/src/modal-type-theory/flat-dependent-pair-types.lagda.md
@@ -87,7 +87,4 @@ module _
## References
-- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type
- theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584))
-- Dan Licata, _cohesion-agda_, GitHub repository
- ()
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-modality.lagda.md b/src/modal-type-theory/flat-modality.lagda.md
index 56863c0e9c..9ae682fecf 100644
--- a/src/modal-type-theory/flat-modality.lagda.md
+++ b/src/modal-type-theory/flat-modality.lagda.md
@@ -169,7 +169,4 @@ module _
## References
-- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type
- theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584))
-- Dan Licata, _cohesion-agda_, GitHub repository
- ()
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-sharp-adjunction.lagda.md b/src/modal-type-theory/flat-sharp-adjunction.lagda.md
index e0a4795a23..7a249c4771 100644
--- a/src/modal-type-theory/flat-sharp-adjunction.lagda.md
+++ b/src/modal-type-theory/flat-sharp-adjunction.lagda.md
@@ -288,7 +288,4 @@ is-uniquely-eliminating-sharp X P .pr2 .pr2 f =
## References
-- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type
- theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584))
-- Dan Licata, _cohesion-agda_, GitHub repository
- ()
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/sharp-modality.lagda.md b/src/modal-type-theory/sharp-modality.lagda.md
index 52610974df..6788e8ef3a 100644
--- a/src/modal-type-theory/sharp-modality.lagda.md
+++ b/src/modal-type-theory/sharp-modality.lagda.md
@@ -212,9 +212,5 @@ ap-sharp f = rec-sharp (unit-sharp ∘ f)
## References
-- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type
- theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584))
-- Dan Licata, _cohesion-agda_, GitHub repository
- ()
-- Felix Cherubini, _DCHoTT-Agda_/Im.agda, file in GitHub repository
- ()
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
+{{#reference Felixwellen/DCHoTT-Agda}}
diff --git a/src/order-theory/galois-connections.lagda.md b/src/order-theory/galois-connections.lagda.md
index 7866ef433f..111bc3090a 100644
--- a/src/order-theory/galois-connections.lagda.md
+++ b/src/order-theory/galois-connections.lagda.md
@@ -545,5 +545,4 @@ module _
## References
-- Erné, Koslowski, Melton, Strecker. _A primer on Galois connections_. Annals
- New York Academy of Sciences 704 (1993)
+{{#bibliography}} {{#reference EKMS93}}
diff --git a/src/orthogonal-factorization-systems/cd-structures.lagda.md b/src/orthogonal-factorization-systems/cd-structures.lagda.md
index 6413398d29..3fcfbb6f4c 100644
--- a/src/orthogonal-factorization-systems/cd-structures.lagda.md
+++ b/src/orthogonal-factorization-systems/cd-structures.lagda.md
@@ -75,6 +75,4 @@ module _
## References
-- Vladimir Voevodsky. _Unstable motivic homotopy categories in Nisnevich and
- cdh-topologies_. Journal of Pure and Applied Algebra 214 8. 2010.
- [arXiv:0805.4576](https://arxiv.org/abs/0805.4576)
+{{#bibliography}} {{#reference Voe10}}
diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
index bdbd345410..cb391dfbff 100644
--- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
@@ -118,7 +118,4 @@ module _
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
index 5875a25b02..aa145fda24 100644
--- a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
+++ b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
@@ -153,10 +153,7 @@ module _
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
## See also
diff --git a/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md
index de1aea3a8f..4ff943dd58 100644
--- a/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md
@@ -191,5 +191,4 @@ module _
## References
-- Felix Cherubini, _DCHoTT-Agda_/Im.agda, file in GitHub repository
- ()
+{{#bibliography}} {{#reference Felixwellen/DCHoTT-Agda}}
diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
index 268ae3b349..ac69913f80 100644
--- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md
@@ -531,7 +531,4 @@ The equivalent notions of
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/orthogonal-factorization-systems/localizations-maps.lagda.md b/src/orthogonal-factorization-systems/localizations-maps.lagda.md
index afdb8a9d4b..265f973ff8 100644
--- a/src/orthogonal-factorization-systems/localizations-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-maps.lagda.md
@@ -89,9 +89,4 @@ It remains to construct a converse.
## References
-1. Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
-2. Egbert Rijke, _Classifying Types_
- ([arXiv:1906.09435](https://arxiv.org/abs/1906.09435))
+{{#bibliography}} {{#reference RSS20}} {{#reference Rij19}}
diff --git a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md
index d5903a78da..9da1074c37 100644
--- a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md
@@ -116,9 +116,4 @@ This is Proposition 5.1.2 in _Classifying Types_, and remains to be formalized.
## References
-1. Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
-2. Egbert Rijke, _Classifying Types_
- ([arXiv:1906.09435](https://arxiv.org/abs/1906.09435))
+{{#bibliography}} {{#reference RSS20}} {{#reference Rij19}}
diff --git a/src/orthogonal-factorization-systems/modal-operators.lagda.md b/src/orthogonal-factorization-systems/modal-operators.lagda.md
index 6f6a038a5e..457aeddced 100644
--- a/src/orthogonal-factorization-systems/modal-operators.lagda.md
+++ b/src/orthogonal-factorization-systems/modal-operators.lagda.md
@@ -146,7 +146,4 @@ module _
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md
index e349c31f79..ccdba0c7e2 100644
--- a/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md
@@ -240,10 +240,7 @@ This remains to be shown.
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
## External links
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index 971e36e5dd..9c1d91990e 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -1081,6 +1081,4 @@ module _
## References
-- Ulrik Buchholtz and Jonathan Weinberger, _Synthetic fibered (∞, 1)-category
- theory_ (2023) ([arXiv:2105.01724](https://arxiv.org/abs/2105.01724),
- [DOI:10.21136/HS.2023.04](https://articles.math.cas.cz/10.21136/HS.2023.04))
+{{#bibliography}} {{#reference BW23}}
diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
index 5518eb7d81..d5daedfeb3 100644
--- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md
+++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
@@ -522,8 +522,4 @@ A wikidata identifier for this concept is unavailable.
## References
-- Emily Riehl and Dominic Verity. _Elements of `∞`-category theory_. Cambridge
- Studies in Advanced Mathematics 194. Cambridge University Press,
- Cambridge, 2022.
- [doi:10.1017/9781108936880](https://doi.org/10.1017/9781108936880). ISBN:
- 978-1-108-83798-9.
+{{#bibliography}} {{#reference Rie22}}
diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
index 6b35ebe7ee..c1f2dc95bd 100644
--- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
@@ -240,12 +240,4 @@ module _
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
-2. Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
-3. Egbert Rijke, _Classifying Types_
- ([arXiv:1906.09435](https://arxiv.org/abs/1906.09435))
+{{#bibliography}} {{#reference UF13}} {{#reference RSS20}} {{#reference Rij19}}
diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/separated-types.lagda.md
index 965dcad305..995088d422 100644
--- a/src/orthogonal-factorization-systems/separated-types.lagda.md
+++ b/src/orthogonal-factorization-systems/separated-types.lagda.md
@@ -37,5 +37,4 @@ module _
## References
-1. Egbert Rijke, _Classifying Types_
- ([arXiv:1906.09435](https://arxiv.org/abs/1906.09435))
+{{#bibliography}} {{#reference Rij19}}
diff --git a/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md
index 1f845ce440..08cd6c74fc 100644
--- a/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/sigma-closed-reflective-subuniverses.lagda.md
@@ -49,7 +49,4 @@ The equivalent notions of
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md
index 7a42c85792..2d9c5958c2 100644
--- a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md
@@ -46,7 +46,4 @@ The equivalent notions of
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
index f4627ce47f..2857183224 100644
--- a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md
@@ -204,7 +204,4 @@ The equivalent notions of
## References
-- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type
- theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020
- ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526),
- [DOI:10.23638/LMCS-16(1:2)2020](https://doi.org/10.23638/LMCS-16%281%3A2%292020))
+{{#bibliography}} {{#reference RSS20}}
diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md
index f50b97b7c0..dafcfa1a66 100644
--- a/src/real-numbers/dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/dedekind-real-numbers.lagda.md
@@ -514,10 +514,9 @@ module _
## References
-1. Section 11.2 of Univalent Foundations Project, _Homotopy Type Theory –
- Univalent Foundations of Mathematics_ (2013)
- ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
+This page follows parts of Section 11.2 in {{#cite UF13}}.
+
+{{#bibliography}}
## External links
diff --git a/src/ring-theory/cyclic-rings.lagda.md b/src/ring-theory/cyclic-rings.lagda.md
index 00456a2c8a..e3b3ac6fca 100644
--- a/src/ring-theory/cyclic-rings.lagda.md
+++ b/src/ring-theory/cyclic-rings.lagda.md
@@ -67,7 +67,7 @@ the nonunital cyclic rings: Cyclic unital rings are
[quotients](ring-theory.quotient-rings.md) of the
[ring `ℤ` of integers](elementary-number-theory.ring-of-integers.md), whereas
cyclic nonunital rings are isomorphic to [ideals](ring-theory.ideals-rings.md)
-of quotients of the ring `ℤ` \[1\].
+of quotients of the ring `ℤ`. {{#cite BSCS05}}
Since cyclic rings are quotients of `ℤ`, it follows that quotients of cyclic
rings are cyclic rings.
@@ -498,5 +498,4 @@ module _
## References
-- \[1\] Maria Balintne-Szendrei, Gabor Czedli, and Agnes Szendrei. _Absztrakt
- algebrai feladatok (Exercises in Abstract Algebra)_. Polygon, Szeged, 2005.
+{{#bibliography}}
diff --git a/src/set-theory/cumulative-hierarchy.lagda.md b/src/set-theory/cumulative-hierarchy.lagda.md
index 95866ae5ba..b908befe92 100644
--- a/src/set-theory/cumulative-hierarchy.lagda.md
+++ b/src/set-theory/cumulative-hierarchy.lagda.md
@@ -762,9 +762,4 @@ needed.
## References
-1. Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations
- of Mathematics_ (2013) ([website](https://homotopytypetheory.org/book/),
- [arXiv:1308.0729](https://arxiv.org/abs/1308.0729))
-2. Tom de Jong, in collaboration with Nicolai Kraus, Fredrik Nordvall Forsberg
- and Chuangjie Xu.
-
+{{#bibliography}} {{#reference UF13}} {{#reference JKFC23}}
diff --git a/src/structured-types/central-h-spaces.lagda.md b/src/structured-types/central-h-spaces.lagda.md
index bdf28b3959..c0ea967513 100644
--- a/src/structured-types/central-h-spaces.lagda.md
+++ b/src/structured-types/central-h-spaces.lagda.md
@@ -41,6 +41,4 @@ is-central-h-space A =
## References
-- Ulrik Buchholtz, Daniel Christensen, Jarl G. Taxerås Flaten, Egbert Rijke,
- _Central H-spaces and banded types_
- ([arXiv:2301.02636](https://arxiv.org/abs/2301.02636))
+{{#bibliography}} {{#reference BCFR23}}
diff --git a/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md b/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md
index 585c51dd1a..6d7f7a1902 100644
--- a/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md
+++ b/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md
@@ -45,8 +45,8 @@ In one direction, our proof relies on the following group-theoretic fact: the
map of [generators](group-theory.generating-elements-groups.md) from a
[set](foundation-core.sets.md) `X` to the free group on `X` is
[injective](foundation-core.injective-maps.md). This is proved constructively in
-\[MRR88\] by Mines, Richman and Ruitenburg, and carried out in HoTT/UF and
-formalized in Agda in \[BCDE21\] by Bezem, Coquand, Dybjer and Escardó.
+{{#cite MRR88}} by Mines, Richman and Ruitenburg, and carried out in HoTT/UF and
+formalized in Agda in {{#cite BCDE21}} by Bezem, Coquand, Dybjer, and Escardó.
Translated to [concrete groups](group-theory.concrete-groups.md) this means that
for every set `X`, we have a [pointed](structured-types.pointed-types.md)
@@ -55,7 +55,7 @@ for every set `X`, we have a [pointed](structured-types.pointed-types.md)
this in our proof below.)
A construction on the level of concrete groups can be found in the recent
-preprint \[Wär23\] by David Wärn.
+preprint by David Wärn {{#cite Warn23draft}}.
For the time being, we haven't formalized this group-theoretic fact; instead we
label it as an explicit assumption of our proof.
@@ -153,14 +153,7 @@ module _
## References
-- \[BCDE21\]: Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó. Free
- groups in HoTT/UF in Agda.
- . 2021.
-- \[MRR88\]: Ray Mines, Fred Richman and Wim Ruitenburg. A Course in
- Constructive Algebra. Universitext. Springer, 1988.
- [doi:10.1007/978-1-4419-8640-5](https://doi.org/10.1007/978-1-4419-8640-5).
-- \[Wär23\]: David Wärn. Path spaces of pushouts. Preprint.
- . 2023.
+{{#bibliography}}
## See also
diff --git a/src/synthetic-homotopy-theory/cavallos-trick.lagda.md b/src/synthetic-homotopy-theory/cavallos-trick.lagda.md
index a147b24389..86e8cc6610 100644
--- a/src/synthetic-homotopy-theory/cavallos-trick.lagda.md
+++ b/src/synthetic-homotopy-theory/cavallos-trick.lagda.md
@@ -63,5 +63,6 @@ module _
- Cavallo's trick was originally formalized in the
[cubical agda library](https://agda.github.io/cubical/Cubical.Foundations.Pointed.Homogeneous.html).
- The above generalization was found by Buchholtz, Christensen, Rijke, and
- Taxerås Flaten, in
- [Central H-spaces and banded types](https://arxiv.org/abs/2301.02636)
+ Taxerås Flaten, in {{#cite BCFR23}}.
+
+{{#bibliography}}
diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
index b0d4a02531..8b3421dddb 100644
--- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -448,8 +448,4 @@ module _
## References
-1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential
- Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE
- Symposium on Logic in Computer Science (LICS '20). Association for Computing
- Machinery, New York, NY, USA, 845–858,
- [DOI:10.1145](https://doi.org/10.1145/3373718.3394801)
+{{#bibliography}} {{#reference SDR20}}
diff --git a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
index f9683868c3..7cafe2e7ee 100644
--- a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
@@ -165,8 +165,4 @@ module _
## References
-1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential
- Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE
- Symposium on Logic in Computer Science (LICS '20). Association for Computing
- Machinery, New York, NY, USA, 845–858,
- [DOI:10.1145](https://doi.org/10.1145/3373718.3394801)
+{{#bibliography}} {{#reference SDR20}}
diff --git a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
index 61cd54ef3b..d4acb85496 100644
--- a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
@@ -792,8 +792,4 @@ module _
## References
-1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential
- Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE
- Symposium on Logic in Computer Science (LICS '20). Association for Computing
- Machinery, New York, NY, USA, 845–858,
- [DOI:10.1145](https://doi.org/10.1145/3373718.3394801)
+{{#bibliography}} {{#reference SDR20}}
diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
index c2fd712d7b..6d1e096c00 100644
--- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
@@ -391,5 +391,4 @@ module _
## References
-- Egbert Rijke, _The join construction_, 2017
- ([arXiv:1701.07538](https://arxiv.org/abs/1701.07538))
+{{#bibliography}} {{#reference Rij17}}
diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
index e4c06b0003..e8bb0099c2 100644
--- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md
@@ -72,5 +72,4 @@ map-Prespectrum A B =
## References
-- J. P. May, _A Concise Course in Algebraic Topology_, 1999
- ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
+{{#bibliography}} {{#reference May99}}
diff --git a/src/synthetic-homotopy-theory/prespectra.lagda.md b/src/synthetic-homotopy-theory/prespectra.lagda.md
index 419d94f51f..b4318725d3 100644
--- a/src/synthetic-homotopy-theory/prespectra.lagda.md
+++ b/src/synthetic-homotopy-theory/prespectra.lagda.md
@@ -114,5 +114,4 @@ module _
## References
-- J. P. May, _A Concise Course in Algebraic Topology_, 1999
- ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
+{{#bibliography}} {{#reference May99}}
diff --git a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
index 884f2074cb..33166e8430 100644
--- a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
@@ -90,8 +90,4 @@ module _
## References
-1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential
- Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE
- Symposium on Logic in Computer Science (LICS '20). Association for Computing
- Machinery, New York, NY, USA, 845–858,
- [DOI:10.1145](https://doi.org/10.1145/3373718.3394801)
+{{#bibliography}} {{#reference SDR20}}
diff --git a/src/synthetic-homotopy-theory/sequentially-compact-types.lagda.md b/src/synthetic-homotopy-theory/sequentially-compact-types.lagda.md
index 9374a9c1e6..bd20d04559 100644
--- a/src/synthetic-homotopy-theory/sequentially-compact-types.lagda.md
+++ b/src/synthetic-homotopy-theory/sequentially-compact-types.lagda.md
@@ -49,5 +49,4 @@ module _
## References
-- Egbert Rijke, _Classifying Types_
- ([arXiv:1906.09435](https://arxiv.org/abs/1906.09435))
+{{#bibliography}} {{#reference Rij19}}
diff --git a/src/synthetic-homotopy-theory/spectra.lagda.md b/src/synthetic-homotopy-theory/spectra.lagda.md
index 6dfba54ea5..8ef4d35b61 100644
--- a/src/synthetic-homotopy-theory/spectra.lagda.md
+++ b/src/synthetic-homotopy-theory/spectra.lagda.md
@@ -139,5 +139,4 @@ module _
## References
-- J. P. May, _A Concise Course in Algebraic Topology_, 1999
- ([pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf))
+{{#bibliography}} {{#reference May99}}
diff --git a/website/css/bibliography.css b/website/css/bibliography.css
new file mode 100644
index 0000000000..457f69439f
--- /dev/null
+++ b/website/css/bibliography.css
@@ -0,0 +1,30 @@
+/* Reset for any previous styles to ensure consistent starting point */
+.bibliography * {
+ box-sizing: border-box;
+}
+
+/* Container style to handle bibliography entries */
+.bibliography dl {
+ width: 100%;
+}
+
+/* Style for the label (dt) */
+.bibliography dt {
+ float: left; /* Float label to the left */
+ font-weight: bold; /* Make label bold */
+ width: 9ch; /* Set fixed width for label */
+ clear: both; /* Ensure label is on its own line and not affected by previous floats */
+ text-align: right;
+ padding-right: 0.5ch;
+}
+
+/* Style for the content (dd) */
+.bibliography dd {
+ margin-left: 9.5ch; /* Offset content to the right of the label */
+ padding-right: 1em; /* Provide some padding for legibility */
+}
+
+/* Specifically targets elements with the .citation-link class to style links */
+.citation-link {
+ text-decoration: none; /* Removes the underline from links */
+}
diff --git a/website/js/custom.js b/website/js/custom.js
index 53ac7ab21c..edc0fb5dcb 100644
--- a/website/js/custom.js
+++ b/website/js/custom.js
@@ -5,6 +5,7 @@ if (link) {
const fileList = [
'ART.md',
'CITE-THIS-LIBRARY.md',
+ 'CITING-SOURCES.md',
'CODINGSTYLE.md',
'CONTRIBUTING.md',
'CONTRIBUTORS.md',