nLab Peter Dybjer

Selected writings

Selected writings

Introducing the notion of inductive types and inductive families in type theory:

On categorical models of dependent types:

Generalization of inductive types to inductive-recursive types:

For moree see:

On internal type theory:

On the categorical semantics of W-types by initial algebras over an endofunctor:

On the categorical model of dependent types by locally cartesian closed categories:

category: people

Last revised on January 22, 2023 at 16:17:42. See the history of this page for a list of all contributions to it.