research
∙
10/15/2022
A tutorial on implementing De Morgan cubical type theory
This tutorial explains (one way) how to implement De Morgan cubical type...
share
research
∙
07/28/2021
Type theories in category theory
We introduce basic notions in category theory to type theorists, includi...
research
∙
05/31/2021
Elegant elaboration with function invocation
We present an elegant design of the core language in a dependently-typed...
research
∙
03/29/2021