Abstracts.2019.CwFs

Categories with Families: Unityped, Simply Typed, and Dependently Typed

by Peter Dybjer

Abstract

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with families (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type.

This is joint work with Simon Castellan, IRISA Rennes and Pierre Clairambault, ENS Lyon.

References

1. Simon Castellan, Pierre Clairambault, Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed. 2019. Foundations and Applications of Univalent Mathematics slides, arXiv preprint.