nLab Robert Seely

• webpage

Selected writings

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

• Robert A. G. Seely, Hyperdoctrines, Natural Deduction and the Beck Condition, Zeitschr. f. math. Logik und Grundlagen d. Math. 29 (1983) 505-542 [doi:10.1002/malq.19830291005, pdf]

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. 95 (1984) 33-48 [doi:10.1017/S0305004100061284, pdf]

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

• R. A. G. Seely, Linear logic, $\ast$-autonomous categories and cofree coalgebras, in Categories in Computer Science and Logic, Contemporary Mathematics 92 (1989) [pdf, ps.gz, ISBN:978-0-8218-5100-5]

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

• R. F. Blute , J. R. B. Cockett, R. A. G. Seely, ! and ? – Storage as tensorial strength, Mathematical Structures in Computer Science 6 4 (1996) 313-351 [doi:10.1017/S0960129500001055]

On 2-type theory:

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

Introducing differential categories:

• R. F. Blute, J. R. B. Cockett, and R. A. G. Seely: Differential categories. Math. Struct. Comput. Sci. 16(06), 1049–1083 (2006) (doi:10.1017/S0960129506005676)

• Richard Blute, Robin Cockett, Jean-Simon Lemay and Robert Seely, Differential categories revisited, Appl. Categ. Struct. 28, 171-235 (2020). (arXiv:1806.04804, doi:10.1007/s10485-019-09572-y)

Related $n$Lab entries

• relation between category theory and type theory

• categorical model of dependent types

• internal logic