2 papers
math.CT2020
A Note on Generalized Algebraic Theories and Categories with Families
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structu…
cs.LO2019
Categories with Families: Unityped, Simply Typed, and Dependently Typed
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we i…