From e3a74c914fc48e5db4d721396deb7eaa05b8315e Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 2 Feb 2024 13:55:24 +0000
Subject: [PATCH] [ 101 ] recording of conor's talk

---
 _101.json | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/_101.json b/_101.json
index 7baf0499..8c3c557f 100644
--- a/_101.json
+++ b/_101.json
@@ -187,7 +187,13 @@
     "title": "Presheaves on Purpose",
     "abstract": "Dependently typed programming languages allow us to define indexed families of datatypes, e.g. <code>Term (n : Nat) : Set</code> as the type of lambda-terms with <code>n</code> variables free. As declared, <code>Term</code> is functorial only on the discrete structure of <code>Nat</code>, which is to say that it respects equality and nobody will faint with amazement. But by an outrageous coincidence (which I learned from Altenkirch, Hofmann and Streicher), such terms can be acted on by <em>thinnings</em> from <code>n</code> to some larger scope <code>m</code>, allowing us to carry terms under binders. That is, we can demonstrate by honest toil that <code>Term</code> is a functor from <code>Thin</code> to <code>Set</code>. I dislike honest toil, and will show you how to design it away in this and similar situations. To that end, I present a universe construction for descriptions of datatypes indexed over the objects of some category <code>C</code> which, by construction, extend to a functors from <code>C</code> to <code>Set</code>, a.k.a. presheaves on <code>Cop</code>.",
     "location": "LT401 and Online",
-    "material": []
+    "material":  [
+      {
+        "tag": "Link",
+        "address": "https://www.youtube.com/watch?v=3gef0_NFz8Q",
+        "linkDescription": "Video"
+      }
+    ]
   },
   {
     "tag": "Talk",