Squashed commit of the following:

commit 6f8fdc1 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 23:22:39 2023 +0200 hom-types are homs commit d7cffc3 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 23:10:50 2023 +0200 `is-set-hom` commit 3a646ce Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 22:53:24 2023 +0200 fix hom-set function categories commit 3bfc7dd Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 22:49:08 2023 +0200 rename hom-sets to `hom-set` commit fd15e21 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 21:42:14 2023 +0200 some comments commit a95c86c Author: Egbert Rijke <[email protected]> Date: Thu Sep 21 12:59:34 2023 +0200 The classification of cyclic rings (UniMath#757) Co-authored-by: izak <[email protected]> commit df1e6e6 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 14:20:56 2023 +0200 consistencies commit 04cf136 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 14:14:52 2023 +0200 add projections initial and terminal objects commit 2ac83c1 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:42:50 2023 +0200 Functors _between_ large... commit 5577dbb Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:33:03 2023 +0200 functors _between_ categories commit 786664f Merge: e0f6858 da7e412 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:26:28 2023 +0200 Merge branch 'master' into functor-categories commit e0f6858 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 02:08:26 2023 +0200 pre-commit commit 3933794 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 02:06:48 2023 +0200 the functor category and natural isomorphisms commit da7e412 Author: Vojtěch Štěpančík <[email protected]> Date: Wed Sep 20 19:01:16 2023 +0200 Coforks, coequalizers of types, their flattening lemma (UniMath#792) This PR introduces coforks of parallel maps, the dependent and non-dependent universal properties of coequalizers, the construction of coequalizers from pushouts, and the flattening lemma for coequalizers, asserting that sigmas commute with coequalizers. This development mirrors the development of cocones and pushouts. I also changed the statement of the flattening lemma for pushouts to one that sounds more natural to me - we can construct a cocone of sigma types from any cocone, not just a pushout; the previous definition required the vertex to be a pushout in those definitions. Now the statement is "if a cocone is a pushout, then the cocone derived from it is a pushout too". commit d9a8a02 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 03:07:19 2023 +0200 refactor isomorphisms in small (pre-)categories commit f47cf60 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:54:35 2023 +0200 `is-iso` to `is-iso-hom` commit 7955721 Merge: d1a36f7 eda7bb2 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:31:31 2023 +0200 Merge remote-tracking branch 'agda-unimath/master' into functor-categories commit d1a36f7 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:29:10 2023 +0200 preliminary extensionality of functors commit 30bfd00 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:30:00 2023 +0200 split up definition `functor-precategory-Precategory` commit 3e22d2a Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:14:06 2023 +0200 a little refactoring of natural transformations commit a9f5f27 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:13:08 2023 +0200 Use `C` instead of `P` dependent products of precategories commit eda7bb2 Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 22:01:57 2023 +0200 Isomorphisms in large categories and large precategories (UniMath#791) commit cdc008d Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 13:19:50 2023 +0200 Add a dot after the sentence "Content created by..." (UniMath#790) commit a081293 Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 13:01:42 2023 +0200 Add the universal property of identity systems to the overview tables (UniMath#789) commit fec9c63 Merge: 65483f6 9d2c235 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 02:26:31 2023 +0200 Merge branch 'master' into functor-categories commit 65483f6 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 02:25:24 2023 +0200 `comp-natural-transformation-Large-Precategory` and associated refactoring commit 9c166ae Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 00:05:11 2023 +0200 pre-commit commit 08af608 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 00:00:34 2023 +0200 prepend `map-` to `(obj/hom)-functor` commit 43ee8e8 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:47:47 2023 +0200 small fixes commit 51ec628 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:21:34 2023 +0200 misc cleanup natural transformations commit 8e6f821 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:19:43 2023 +0200 define representing arrow category commit 9d2c235 Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 15:52:57 2023 +0200 Fix website CI (UniMath#786) commit 1bea263 Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 09:52:52 2023 +0200 Always enable git metadata, fetch whole git history in pages CI (UniMath#785) commit b1f027f Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 03:25:35 2023 +0200 Try to fix website CI (UniMath#784) commit 6af959b Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 03:01:42 2023 +0200 Automatically extract page contributor information during web build (UniMath#770) commit b66c539 Merge: 47f04e3 539174a Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 01:19:20 2023 +0200 Merge branch 'UniMath:master' into functor-categories commit 47f04e3 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 01:18:42 2023 +0200 links functors between categories commit 539174a Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 00:39:14 2023 +0200 Yoneda's lemma for categories (UniMath#783) commit 0106784 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 18:05:43 2023 +0200 Moving file about hexagons of identifications (UniMath#782) commit b804ea5 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:45:44 2023 +0200 Update README.md (UniMath#781) commit f7d6658 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:24:59 2023 +0200 Update README.md (UniMath#780) commit f4f4ef2 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:13:37 2023 +0200 Update README.md (UniMath#779) commit 6df85b4 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:08:03 2023 +0200 Fancy title on repo page (UniMath#778) commit 1fb5dc5 Author: maybemabeline <[email protected]> Date: Sat Sep 16 22:32:19 2023 +0200 Equivalence between the first sphere and the circle (UniMath#776) Co-authored-by: Egbert Rijke <[email protected]> commit 1fe0803 Author: Fredrik Bakke <[email protected]> Date: Fri Sep 15 16:18:37 2023 +0200 Define representations of monoids (UniMath#765) commit c813a06 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 15:17:44 2023 +0200 larger image, rounded corners (UniMath#774) commit 0529896 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 13:23:30 2023 +0200 update contributors (UniMath#773) commit 5340335 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 10:58:02 2023 +0200 update contributors, remove unused imports (UniMath#772) commit 533cff1 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 01:08:32 2023 +0200 Adding an art page (UniMath#771) Co-authored-by: Andrej Bauer <[email protected]> Co-authored-by: Matej Petković <[email protected]> commit adf864e Author: Egbert Rijke <[email protected]> Date: Thu Sep 14 16:44:32 2023 +0200 Symmetric core of a relation (UniMath#754) In this PR we construct the symmetric core of a type valued relation and show that it is the right adjoint of the restriction functor from symmetric relations to relations. Everything we do in this PR is fully coherent and untruncated. --------- Co-authored-by: Fredrik Bakke <[email protected]> commit 50fdf54 Author: Egbert Rijke <[email protected]> Date: Wed Sep 13 19:11:14 2023 +0200 The one-object precategory of a monoid (UniMath#766) commit 413a1bf Author: Vojtěch Štěpančík <[email protected]> Date: Wed Sep 13 18:35:55 2023 +0200 Flattening lemma for pushouts (UniMath#764) commit d826323 Author: Egbert Rijke <[email protected]> Date: Wed Sep 13 17:00:53 2023 +0200 rational commutative monoids (UniMath#763) This small PR factors out rational commutative monoids from UniMath#623. --------- Co-authored-by: Fredrik Bakke <[email protected]>
fredrik-bakke · Sep 21, 2023 · a6b6523 · a6b6523
1 parent 3987828
commit a6b6523
Show file tree

Hide file tree

Showing 405 changed files with 17,764 additions and 4,425 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -71,6 +71,17 @@ jobs:
           path: master/_build
           key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
 
+      # Install Python and friends for website generation only where needed
+      - uses: actions/setup-python@v4
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        with:
+          python-version: '3.8'
+          check-latest: true
+          cache: 'pip'
+
+      - run: python3 -m pip install -r master/scripts/requirements.txt
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+
       # We need to run the sources through Agda not only to get the highlighting
       # (which is irrelevant for checking links), but because it flattens the
       # directory structure to a format which is expected in the links we write.
@@ -150,7 +161,7 @@ jobs:
 
       - uses: actions/setup-python@v4
         with:
-          python-version: '3.11.1'
+          python-version: '3.8'
           check-latest: true
           cache: 'pip'
 

diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -40,10 +40,8 @@ jobs:
         uses: actions/checkout@v3
         with:
           path: master
-
-      - uses: r-lib/actions/setup-pandoc@v2
-        with:
-          pandoc-version: '3.0.1'
+          # We need the entire history for contributor information
+          fetch-depth: 0
 
       - name: Setup Agda
         uses: wenkokke/[email protected]
@@ -88,13 +86,15 @@ jobs:
 
       - uses: actions/setup-python@v4
         with:
-          python-version: '3.11.1'
+          python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r master/scripts/requirements.txt
 
       - name: Generate book
+        env:
+          MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE: 'true'
         run: |
           cd master
           make website

diff --git a/.gitignore b/.gitignore
@@ -419,10 +419,13 @@ node_modules/*
 .rvmrc
 package-lock.json
 
-# mdbook
+# mdbook, automatically generated files
 docs/
 html/
 book/
 src/temp/
 src/everything.lagda.md
 SUMMARY.md
+CONTRIBUTORS.md
+MAINTAINERS.md
+/website/css/Agda-highlight.css
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -101,6 +101,7 @@ repos:
     hooks:
       - id: autopep8
         name: Python scripts formatting
+        args: ['-i', '--global-config', '/dev/null']
 
   - repo: https://github.com/pre-commit/mirrors-prettier
     rev: 'v3.0.0-alpha.6'

diff --git a/ART.md b/ART.md
@@ -0,0 +1,8 @@
+# Agda-unimath art
+
+<div align="center" style="margin: 2em 0;">
+  <figure>
+    <img src="website/images/agda-unimath-black-and-gold.png" alt="The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023" width="95%" style="border-radius: 10px;">
+    <figcaption>The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023</figcaption>
+  </figure>
+</div>
diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md
diff --git a/HOME.md b/HOME.md
@@ -5,7 +5,7 @@ at formalizing mathematics from a univalent point of view using the dependently
 typed programming language [Agda](https://github.com/agda/agda).
 
 <a href="https://github.com/unimath/agda-unimath">
-<img align="right" width="300" alt="agda-unimath" src="agda-unimath-logo.svg" />
+<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 Bonnevier, Jonathan Prieto-Cubides,
@@ -34,7 +34,3 @@ Follow the instructions in our [installation guide](HOWTO-INSTALL.md) to set up
 the project. After you have completed your formalization, submit it via a pull
 request. We will review your contribution and work towards incorporating it into
 the `agda-unimath` library.
-
-{{#include SUMMARY.md}}
-
-{{#include CONTRIBUTORS.md}}
diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
@@ -21,7 +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. `pre-commit` and `request`. Those two programs can be installed by running
+4. The python libraries `pre-commit`, `requests` and `tomli`. Those can be
+   installed by running
    ```shell
    python3 -m pip install -r scripts/requirements.txt
    ```

diff --git a/MAINTAINERS.md b/MAINTAINERS.md
diff --git a/Makefile b/Makefile
@@ -5,12 +5,14 @@ AGDAVERBOSE ?= -v1
 # use "$ export AGDAVERBOSE=20" if you want to see all
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)
 AGDAMDFILES := $(subst src/,docs/,$(AGDAFILES:.lagda.md=.md))
+CONTRIBUTORS_FILE := ./scripts/contributors_data.toml
 
 AGDAHTMLFLAGS ?= --html --html-highlight=code --html-dir=docs --css=Agda.css --only-scope-checking
 AGDA ?= agda $(AGDAVERBOSE)
 TIME ?= time
 
 METAFILES := \
+  ART.md \
   CITE-THIS-LIBRARY.md \
   CODINGSTYLE.md \
   CONTRIBUTING.md \
@@ -67,20 +69,32 @@ agda-html: ./src/everything.lagda.md
 	@mkdir -p ./docs/
 	@${AGDA} ${AGDAHTMLFLAGS} ./src/everything.lagda.md
 
-SUMMARY.md: ${AGDAFILES}
+SUMMARY.md: ${AGDAFILES} ./scripts/generate_main_index_file.py
 	@python3 ./scripts/generate_main_index_file.py
 
+MAINTAINERS.md: ${CONTRIBUTORS_FILE} ./scripts/generate_maintainers.py
+	@python3 ./scripts/generate_maintainers.py
+
+CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./scripts/generate_contributors.py
+	@python3 ./scripts/generate_contributors.py
+
+website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppuccin.css
+	@python3 ./scripts/generate_agda_css.py
+
 .PHONY: website-prepare
-website-prepare: agda-html ./SUMMARY.md
+website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md ./website/css/Agda-highlight.css
 	@cp $(METAFILES) ./docs/
-	@cp ./theme/images/agda-unimath-logo.svg ./docs/
+	@mkdir -p ./docs/website
+	@cp -r ./website/images ./docs/website/
+	@cp -r ./website/css ./docs/website/
+	@cp -r ./website/js ./docs/website/
 
 .PHONY: website
 website: website-prepare
 	@mdbook build
 
 .PHONY: serve-website
-serve-website:
+serve-website: website-prepare
 	@mdbook serve -p 8080 --open -d ./book/html
 
 .PHONY: graph

diff --git a/README.md b/README.md
@@ -1,19 +1,17 @@
-# The agda-unimath library
-
-[![CI](https://github.com/UniMath/agda-unimath/actions/workflows/ci.yaml/badge.svg)](https://github.com/UniMath/agda-unimath/actions/workflows/ci.yaml)
-[![agda-unimath website](https://github.com/UniMath/agda-unimath/actions/workflows/pages.yaml/badge.svg)](https://github.com/UniMath/agda-unimath/actions/workflows/pages.yaml)
+# ![The agda-unimath library](https://github.com/UniMath/agda-unimath/assets/1252282/cbd9b67e-581c-41c7-bc1e-34862127bad2)
 
 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 Bonnevier, Jonathan Prieto-Cubides, and Egbert Rijke. 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 Bonnevier, Jonathan Prieto-Cubides, and Egbert Rijke, and
+is also being maintained by Fredrik Bakke. 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
 
-1. [agda-unimath webpage](https://unimath.github.io/agda-unimath/)
+1. [The agda-unimath website](https://unimath.github.io/agda-unimath/)
 2. [Discord](https://discord.gg/Zp2e8hYsuX)
 3. [Twitch](https://www.twitch.tv/agdaunimath)
diff --git a/book.toml b/book.toml
@@ -6,6 +6,7 @@ title = "agda-unimath"
 
 [build]
 create-missing = true
+
 [preprocessor.index]
 
 [preprocessor.links]
@@ -18,28 +19,58 @@ static-css = false
 include-src = false
 block-delimiter = {left = "$$", right = "$$"}
 inline-delimiter = {left = "$", right = "$"}
-macros = "theme/latex-macros.txt"
+macros = "website/latex-macros.txt"
 
 [preprocessor.catppuccin]
 assets_version = "0.2.1" # DO NOT EDIT: Managed by `mdbook-catppuccin install`
 
+[preprocessor.git-metadata]
+command = "python3 ./scripts/preprocessor_git_metadata.py"
+# Disable by default - it takes a non-trivial amount of time
+# Can be overriden by running
+# `export MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE=true` in your shell
+enable = false
+# Only show "Content created by" on Agda source files
+attribute_file_extensions = [ ".lagda.md" ]
+# Don't add anything to the "non-content" pages,
+# i.e. top-level markdown files which aren't guides
+suppress_processing = [
+  "HOME.md",
+  "MAINTAINERS.md",
+  "CONTRIBUTORS.md",
+  "STATEMENT-OF-INCLUSION",
+  "USERS.md",
+  "GRANT-ACKNOWLEDGEMENTS.md",
+  "SUMMARY.md",
+  "ART.md"
+]
+
 [output.linkcheck]
 follow-web-links = false
 
 [output.html]
 default-theme = "light"
 preferred-dark-theme = "Ayu"
 copy-fonts = true
-additional-css = ["theme/Agda.css", "theme/pagetoc.css", "theme/agda-logo.css", "./theme/catppuccin.css", "./theme/catppuccin-highlight.css"]
-additional-js = ["theme/js/custom.js", "theme/pagetoc.js"]
+additional-css = [
+  "website/css/Agda.css",
+  "website/css/Agda-highlight.css",
+  "website/css/agda-logo.css",
+  "theme/catppuccin.css",
+  "theme/catppuccin-highlight.css",
+  "theme/pagetoc.css",
+]
+additional-js = [
+  "website/js/custom.js",
+  "theme/pagetoc.js"
+]
 no-section-label = false
 site-url = "/agda-unimath/"
 git-repository-url = "https://github.com/UniMath/agda-unimath"
 git-repository-icon = "fa-github"
 
 [output.html.print]
-enable = true    # include support for printable output
-page-break = true # insert page-break after each chapter
+enable = false
 
 [output.html.fold]
 enable = true    # whether or not to enable section folding

diff --git a/flake.nix b/flake.nix
@@ -18,7 +18,9 @@
           pkgs = nixpkgs.legacyPackages."${system}";
           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
             requests
+            tomli
           ]);
 
           agda-unimath-package = { lib, mkDerivation, time }: mkDerivation {