nLab
Robert Seely

Selected writings

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

  • R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

… the equivalence between linear logic and star-autonomous categories:

  • R. A. G. Seely, Linear logic, *\ast-autonomous categories and cofree coalgebras, Contemporary Mathematics 92, 1989. (pdf, ps.gz)

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 October 21, 2021 at 08:17:42. See the history of this page for a list of all contributions to it.