Merge branch 'main' into formalize-yoneda-embedding

.github/workflows/format.yml

@@ -1,30 +1,22 @@
-name: Code autoformatting
+name: File formatting
 
 on:
   push:
     branches:
       - main
+  pull_request:
+    branches:
+      - main
 
 jobs:
   format:
     runs-on: ubuntu-latest
-    permissions:
-      contents: write
     steps:
       - name: Checkout code
         uses: actions/checkout@v3
-        with:
-          # Make sure the actual branch is checked out when running on pull requests
-          ref: ${{ github.head_ref }}
-          # This is important to fetch the changes to the previous commit
-          fetch-depth: 0
 
-      - name: Run Prettier
+      - name: Prettier
         uses: creyD/[email protected]
         with:
-          prettier_options: --write **/*.{md,json,yaml,yml}
-          commit_options: --allow-empty
-          # Update the current commit instead of creating a new one. Only works if checkout fetch depth is set to `0`
-          same_commit: true
-          # Prettify changed files. Only works if checkout fetch depth is set to `0`
-          only_changed: true
+          dry: true
+          prettier_options: --check **/*.{md,json,yaml,yml}

.vscode/extensions.json

@@ -1,6 +1,6 @@
 {
-    "recommendations": [
-        "nikolaikudasovfizruk.rzk-1-experimental-highlighting",
-        "esbenp.prettier-vscode"
-    ]
+  "recommendations": [
+    "nikolaikudasovfizruk.rzk-1-experimental-highlighting",
+    "esbenp.prettier-vscode"
+  ]
 }

README.md

@@ -17,7 +17,7 @@ results from the following papers:
 - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)"
   [3]
 
-This formalization project follows the philosophy layed out in the article
+This formalization project follows the philosophy laid out in the article
 "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)"
 [4].