merging the yoneda geodesic

emilyriehl · Jun 25, 2024 · cd1c9e4 · cd1c9e4
2 parents 0628dcd + 88b6183
commit cd1c9e4
Show file tree

Hide file tree

Showing 4 changed files with 822 additions and 2 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -15,7 +15,7 @@
   "editor.inlineSuggest.enabled": true,
   "editor.acceptSuggestionOnEnter": "off",
   "editor.snippetSuggestions": "top",
-  "editor.wordBasedSuggestions": false,
+  "editor.wordBasedSuggestions": "off",
   "javascript.suggest.names": false,
 
   // Autoformatting and file type specific settings

diff --git a/lean/_target/deps/mathlib b/lean/_target/deps/mathlib
diff --git a/mkdocs.yml b/mkdocs.yml
@@ -34,6 +34,7 @@ nav:
       - The Yoneda Lemma: simplicial-hott/09-yoneda.rzk.md
       - ∞-categories (Rezk Types): simplicial-hott/10-rezk-types.rzk.md
       - Cocartesian Families: simplicial-hott/12-cocartesian.rzk.md
+      - Geodesic to the Yoneda lemma: simplicial-hott/13-yoneda-geodesic.rzk.md
 
 markdown_extensions:
   - admonition