3 ms·
Jon Sterling, How to code your own type theory https://www.youtube.com/watch?v=DEj-_k2Nx6o https://www.youtube.com/watch?v=DEj-_k2Nx6o There's Pi and Sigma so
by hackandthink 3y ago
Jon Sterling, How to code your own type theory
https://www.youtube.com/watch?v=DEj-_k2Nx6o 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/main/Colloquia/Sterling/tutorial/lib https://github.com/martinescardo/HoTTEST-Summer-School/tree/...