Jon Sterling, How to code your own type theory https://www.youtube.com/watch?v=D... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		hackandthink on June 15, 2023 \| parent \| context \| favorite \| on: How to implement dependent type theory I (2012) Jon Sterling, How to code your own type theory https://www.youtube.com/watch?v=DEj-_k2Nx6o There's Pi and Sigma so it is about dependent type theory as well. type term = \| Var of var \| Pi of term * term binder (* Pi (x:A). Bx A; x.B ) \| Sg of term term binder https://github.com/martinescardo/HoTTEST-Summer-School/tree/...

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact