nLab Robert Seely

Selected writings

On hyperdoctrines, and natural deduction in categorical logic, and the Beck-Chevalley condition:

On the relation between type theory and category theory

…the equivalence of categories between first order theories and hyperdoctrines:

  • R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für Math. Logik und Grundlagen der Math. (1984) (pdf)

…the equivalence of categories between locally cartesian closed categories and dependent type theories was originally claimed in

… the categorical semantics of linear logic in star-autonomous categories:

On categorical semantics of the exponential modality in linear type theory:

On 2-type theory:

  • R.A.G. Seely, Modeling computations: a 2-categorical framework, LICS 1987 (pdf)

Introducing differential categories:

category: people

Last revised on May 19, 2023 at 12:16:23. See the history of this page for a list of all contributions to it.