From 2496ba67f69c2ac73ac8d6b4857d6afb88c0dec2 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 19 Oct 2024 17:33:38 -0500 Subject: [PATCH] convert link --- .../index.mdx} | 6 +++--- .../content/posts/2024-10-19-cubical-talk/main.pdf | Bin 2 files changed, 3 insertions(+), 3 deletions(-) rename src/content/posts/{2024-10-19-cubical-talk.md => 2024-10-19-cubical-talk/index.mdx} (89%) rename public/talks/2024-10-19-formalizing-mathematics-with-cubical-type-theory.pdf => src/content/posts/2024-10-19-cubical-talk/main.pdf (100%) 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