From 396e1f509821ce8fbbede05ed8385990f39bf230 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 23 Oct 2023 22:22:36 -0500 Subject: [PATCH] not ish --- .../posts/2023-10-23-path-induction-gadt-perspective.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md b/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md index ff43296..775c124 100644 --- a/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md +++ b/src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md @@ -1,5 +1,5 @@ --- -title: "Path induction eliminator: a GADT perspective" +title: "Path induction: a GADT perspective" slug: 2023-10-23-path-induction-gadt-perspective date: 2023-10-23 tags: ["type-theory"] @@ -36,7 +36,7 @@ Like all inductive types, it comes with the typical rules used to introduce type - Computation rule There's something quite peculiar about the elimination rule in particular (commonly known as "path induction", or just $J$). -Let's take a look at its definition, in Agda-ish syntax: +Let's take a look at its definition, in Agda syntax: ```agda J : {A : Set}