Showing 2021Show all
2 papers · 1 filter
cs.LO2021
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…
cs.PL2021
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.