6 papers
(Co)condition hits the Path
Tesla Zhang, Valery Isaev
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax…
Three non-cubical applications of extension types
Tesla Zhang
The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type t…
Two tricks to trivialize higher-indexed families
Tesla Zhang
The conventional general syntax of indexed families in dependent type theories follow the style of "constructors returning a special case", as in Agda, Lean, Idris, Coq, and probab…
A tutorial on implementing De Morgan cubical type theory
Tesla Zhang
This tutorial explains (one way) how to implement De Morgan cubical type theory to people who know how to implement a dependent type theory. It contains an introduction to basic co…
Type theories in category theory
Tesla Zhang
We introduce basic notions in category theory to type theorists, including comprehension categories, categories with attributes, contextual categories, type categories, and categor…
Elegant elaboration with function invocation
Tesla Zhang
We present an elegant design of the core language in a dependently-typed lambda calculus with -reduction and an elaboration algorithm.