michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

not ish
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2023-10-23 22:22:36 -05:00
parent 025437ca10
commit 396e1f5098
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md
View file

@ -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 slug: 2023-10-23-path-induction-gadt-perspective
date: 2023-10-23 date: 2023-10-23
tags: ["type-theory"] tags: ["type-theory"]
@ -36,7 +36,7 @@ Like all inductive types, it comes with the typical rules used to introduce type
- Computation rule - Computation rule
There's something quite peculiar about the elimination rule in particular (commonly known as "path induction", or just $J$). 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 ```agda
J : {A : Set} J : {A : Set}