Abstract

The concept of refinement in type theory is a way of reconciling the “intrinsic” and the “extrinsic” meanings of types (aka “types à la Church” and “types à la Curry”). In a recent paper with Paul-André Melliès¹, we looked at this idea more carefully and settled on the simple conclusion that the type-theoretic notion of “type refinement system” may be identified with the category-theoretic notion of “functor”. This generalization of the traditional analogy (type system ~ category) has the practical benefit, we believe, of bringing the interests of type theory and the tools of categorical logic much closer together. For example, workaday concepts such as “typing judgments”, “subtyping”, and “typing derivations” can be analyzed mathematically on general terms, without having to fix a particular formal system. In the paper, we also use this correspondence to motivate the study of “monoidal closed bifibrations”, which is essentially the type theory induced by combining the usual product and function spaces with inverse image and direct image type constructors. We have found that many interesting new phenomena arise by this simple twist on the simply-typed lambda calculus.

In the talk I will try to motivate and explain these ideas from a relatively elementary perspective (some background in both type theory and categorical logic could be helpful, but either should be sufficient).

refinement and monoidal closed bifibrations", http://arxiv.org/abs/1310.0263