# nLab Robert Seely

## Selected writings

…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)
• R.A.G. Seely, Modeling computations: a 2-categorical framework, LICS 1987 (pdf)

Introducing differential categories:

category: people