diff --git a/src/content/posts/2024-10-19-cubical-talk.md b/src/content/posts/2024-10-19-cubical-talk/index.mdx similarity index 89% rename from src/content/posts/2024-10-19-cubical-talk.md rename to src/content/posts/2024-10-19-cubical-talk/index.mdx index c347100..3039c39 100644 --- a/src/content/posts/2024-10-19-cubical-talk.md +++ b/src/content/posts/2024-10-19-cubical-talk/index.mdx @@ -4,10 +4,10 @@ date: 2024-10-19T21:47:34.026Z tags: [agda, cubical, type-theory, talk] --- -Yesterday I gave my first talk about type theory at my school's grad student seminar series, about some of the work I had been doing with homotopy type theory and cubical Agda. -Here is a link to the [slides]. +import slides from "./main.pdf?url"; -[slides]: ../../talks/2024-10-19-formalizing-mathematics-with-cubical-type-theory.pdf +Yesterday I gave my first talk about type theory at my school's grad student seminar series, about some of the work I had been doing with homotopy type theory and cubical Agda. +Here is a link to the slides. It was not a very great talk so I had a couple of important takeaways. diff --git a/public/talks/2024-10-19-formalizing-mathematics-with-cubical-type-theory.pdf b/src/content/posts/2024-10-19-cubical-talk/main.pdf similarity index 100% rename from public/talks/2024-10-19-formalizing-mathematics-with-cubical-type-theory.pdf rename to src/content/posts/2024-10-19-cubical-talk/main.pdf