blog: rename title

aya-prover · Jun 19, 2024 · bb4065a · bb4065a
1 parent fde7a14
commit bb4065a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/.vitepress/config.mts b/src/.vitepress/config.mts
@@ -45,7 +45,7 @@ export default defineConfig({
           { text: 'TT in TT using QIIT', link: '/blog/tt-in-tt-qiit' },
           { text: 'Extended Pruning', link: '/blog/extended-pruning' },
           { text: 'Farewell, Univalence', link: '/blog/bye-hott' },
-          { text: 'Inductive Props', link: '/blog/ind-prop' },
+          { text: 'Impredicative Props', link: '/blog/ind-prop' },
           { text: 'Def. projection in classes', link: '/blog/class-defeq' },
           { text: 'Path cons. elaboration', link: '/blog/pathcon-elab' },
           { text: 'Path type elaboration', link: '/blog/path-elab' },

diff --git a/src/blog/ind-prop.md b/src/blog/ind-prop.md
@@ -1,4 +1,4 @@
-# Inductive Prop are so wrong!
+# Impredicative Props are hard
 
 Throughout this blog post, I will use the term `Prop` to mean the type of propositions,
 which _does not_ have to be strict, but has the property that it cannot eliminate to `Type`.