Merge branch 'master' into iteration-dependent-functions

CONTRIBUTORS.toml

@@ -12,10 +12,10 @@ displayName = "Egbert Rijke"
 maintainer = true
 extra = " (Lead developer)"
 usernames = [ "Egbert Rijke" ]
-homepage = "https://users.fmf.uni-lj.si/rijke/"
+homepage = "https://egbertrijke.github.io"
 github = "EgbertRijke"
 bio = '''
-Egbert Rijke is a postdoctoral researcher at the University of Ljubljana. His
+Egbert Rijke is a postdoctoral researcher at Johns Hopkins University. His
 research is on homotopy type theory and general mathematics from a univalent
 point of view.
 '''
@@ -35,7 +35,7 @@ in Trondheim. His research is on homotopy type theory and higher category theory
 displayName = "Elisabeth Stenholm"
 maintainer = true
 usernames = [ "Elisabeth Stenholm", "Elisabeth Bonnevier" ]
-homepage = "https://elisabeth.bonnevier.one"
+homepage = "https://elisabeth.stenholm.one"
 github = "elisabethstenholm"
 bio = '''
 Elisabeth is a PhD student at the University of Bergen. Her research is on
@@ -75,16 +75,19 @@ github = "EleonoreMangel"
 displayName = "Bryan Lu"
 usernames = [ "Bryan Lu" ]
 github = "blu-bird"
+homepage = "https://blu-bird.github.io"
 
 [[contributors]]
 displayName = "Raymond Baker"
 usernames = [ "Raymond Baker" ]
 github = "morphismz"
+homepage = "https://morphismz.github.io"
 
 [[contributors]]
 displayName = "Elif Uskuplu"
 usernames = [ "ElifUskuplu" ]
 github = "ElifUskuplu"
+homepage = "https://elifuskuplu.github.io"
 
 [[contributors]]
 displayName = "Victor Blanchi"
@@ -149,6 +152,7 @@ usernames = [ "Julian KG" ]
 displayName = "favonia"
 usernames = [ "favonia" ]
 github = "favonia"
+homepage = "https://favonia.org"
 
 [[contributors]]
 displayName = "fernabnor"
@@ -217,6 +221,7 @@ github = "louismntnu"
 displayName = "Andrej Bauer"
 usernames = [ "Andrej Bauer" ]
 github = "andrejbauer"
+homepage = "https://www.andrej.com"
 
 [[contributors]]
 displayName = "Matej Petković"

DESIGN-PRINCIPLES.md

@@ -29,7 +29,7 @@ makes use of several postulates.
 9. **Pushouts** are postulated in
    [`synthetic-homotopy-theory.pushouts`](synthetic-homotopy-theory.pushouts.md)
 10. **Extensionality of globular types** is postulated in
-    [`structured-types.equality-globular-types`](structured-types.equality-globular-types.md).
+    [`globular-types.equality-globular-types`](globular-types.equality-globular-types.md).
 11. Various **Agda built-in types** are postulated in
     [`primitives`](primitives.md) and in [`reflection`](reflection.md).
 12. The **flat modality** and accompanying modalities, with propositional

GRANT-ACKNOWLEDGEMENTS.md

@@ -1,8 +1,14 @@
 # Grant acknowledgements
 
-If you are doing significant work for the agda-unimath library, such as work
-that leads to a preprint, or a conference or journal submission, then we can
-also acknowledge any research grants you are working under on this page.
+The agda-unimath maintainers and contributors are grateful for funding from the
+following grants:
 
-- The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2020-Present). Air
+- The MURI grant (2024-present). US Air Force Office of Scientific Research,
+  award number FA9550-21-1-0009.
+- The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2021-2024). US Air
   Force Office of Scientific Research, award number FA9550-21-1-0024.
+
+If you are doing significant work for the agda-unimath library, such as work
+that leads to a preprint, or a conference or journal submission, please let us
+know so that we can acknowledge any funding and support you are receiving on
+this page.

HOME.md

@@ -8,14 +8,18 @@ typed programming language [Agda](https://github.com/agda/agda).
 <img class="invertible-image" align="right" width="300" alt="agda-unimath" src="website/images/agda-unimath-logo.svg" />
 </a>
 
-The library project was created by Elisabeth Stenholm, Jonathan Prieto-Cubides,
-and Egbert Rijke, and is currently being maintained by Egbert Rijke, Fredrik
-Bakke, and Vojtěch Štěpančík. Our goal is to create an online encyclopedia of
-formalized mathematics containing an extensive curriculum of topics from a
-univalent point of view. We think libraries of formalized mathematics have the
-potential to be useful, and informative resources for both working and learning
-mathematicians. Our library is designed to work towards this goal, and we
-welcome contributions to the library within any topic in mathematics.
+The library project was created by
+[Elisabeth Stenholm](https://elisabeth.stenholm.one),
+[Jonathan Prieto-Cubides](https://jonaprieto.github.io), and
+[Egbert Rijke](https://egbertrijke.github.io), and is currently being maintained
+by Egbert Rijke, [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke),
+and [Vojtěch Štěpančík](https://vojtechstep.eu/). Our goal is to create an
+online encyclopedia of formalized mathematics containing an extensive curriculum
+of topics from a univalent point of view. We think libraries of formalized
+mathematics have the potential to be useful, and informative resources for both
+working and learning mathematicians. Our library is designed to work towards
+this goal, and we welcome contributions to the library within any topic in
+mathematics.
 
 The agda-unimath library is compatible with Agda 2.6.4 and can be compiled by
 running `make check` from the root directory of the repository. Learn more about

README.md

@@ -2,13 +2,16 @@
 
 The agda-unimath library is a community formalization project for univalent
 mathematics in [Agda](https://github.com/agda/agda). The library project was
-created by Elisabeth Stenholm, Jonathan Prieto-Cubides, and Egbert Rijke, and is
-currently being maintained by Egbert Rijke, Fredrik Bakke, and Vojtěch
-Štěpančík. Our goal is to formalize an extensive curriculum of mathematics from
-the univalent point of view. Furthermore, we think libraries of formalized
-mathematics have the potential to be useful, and informative resources for
-mathematicians. Our library is designed to work towards this goal, and we
-welcome contributions to the library about any topic in mathematics.
+created by [Elisabeth Stenholm](https://elisabeth.stenholm.one),
+[Jonathan Prieto-Cubides](https://jonaprieto.github.io), and
+[Egbert Rijke](https://egbertrijke.github.io), and is currently being maintained
+by Egbert Rijke, [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke),
+and [Vojtěch Štěpančík](https://vojtechstep.eu/). Our goal is to formalize an
+extensive curriculum of mathematics from the univalent point of view.
+Furthermore, we think libraries of formalized mathematics have the potential to
+be useful, and informative resources for mathematicians. Our library is designed
+to work towards this goal, and we welcome contributions to the library about any
+topic in mathematics.
 
 ## Links
 

VISUALIZATION.md

@@ -28,9 +28,11 @@ allows you to determine dependencies between individual definitions. Hover over
   </iframe>
 </div>
 
-The interactive explorer was developed by Job Petrovčič. In addition, Vojtěch
-Štěpančík, Matej Petković, and Andrej Bauer contributed invaluable suggestions
-and offered helpful support.
+The interactive explorer was developed by
+[Job Petrovčič](https://github.com/JobPetrovcic). In addition,
+[Vojtěch Štěpančík](https://vojtechstep.eu/), Matej Petković, and
+[Andrej Bauer](https://www.andrej.com) contributed invaluable suggestions and
+offered helpful support.
 
 ### Notes
 

references.bib

@@ -28,6 +28,22 @@ @article{AKS15
   langid      = {english}
 }
 
+@article{AL19,
+  title       = {Displayed Categories},
+  author      = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter},
+  doi         = {10.23638/LMCS-15(1:20)2019},
+  journal     = {{Logical Methods in Computer Science}},
+  volume      = {15},
+  issue       = {1},
+  year        = {2019},
+  month       = {03},
+  keywords    = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
+  eprint      = {1705.04296},
+  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},
@@ -488,10 +504,27 @@ @misc{Mye21
   primaryclass  = {math.CT}
 }
 
-@online{OEIS,
-  title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})},
-  organization = {{{OEIS}} Foundation Inc.},
-  url          = {https://oeis.org/}
+@online{oeis,
+  title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
+  author       = {OEIS Foundation Inc.},
+  date         = {1996},
+  citeas       = {OEIS},
+  url          = {https://oeis.org},
+  howpublished = {website},
+}
+
+@phdthesis{Qui16,
+  title = {Lawvere–Tierney sheafification in Homotopy Type Theory},
+  author = {Quirin, Kevin},
+  url = {https://kevinquirin.github.io/thesis/main.pdf},
+  year = {2016},
+  month = dec,
+  number = {2016EMNA0298},
+  school = {École des Mines de Nantes},
+  abstract = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis.
+  To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.
+  Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
+  langid = {english}
 }
 
 @book{Rie17,

scripts/markdown_conventions.py

@@ -106,6 +106,10 @@ def find_ill_formed_block(mdcode):
         output = re.sub(
             r'(^|\n)(#+\s.*)[\.,:;!?¡¿]\s*($|\n)', r'\1\2\3', output)
 
+        # Replace strange whitespace with normal spaces
+        output = re.sub(
+            r'(?<!^)(?![ \t\r\n\f\v])\s', r' ', output)
+
         if output != inputText:
             with open(fpath, 'w') as f:
                 f.write(output)

src/category-theory.lagda.md

@@ -38,11 +38,13 @@ open import category-theory.coproducts-in-precategories public
 open import category-theory.cores-categories public
 open import category-theory.cores-precategories public
 open import category-theory.coslice-precategories public
+open import category-theory.dependent-composition-operations-over-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public
 open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
+open import category-theory.displayed-precategories public
 open import category-theory.embedding-maps-precategories public
 open import category-theory.embeddings-precategories public
 open import category-theory.endomorphisms-in-categories public