Type refinement and monoidal closed bifibrations
Abstract
The concept of_refinement_ in type theory is a way of reconciling the "intrinsic" and the "extrinsic" meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of "type refinement system" may be identified with the category-theoretic notion of "functor". We then use this correspondence to give an equivalent type-theoretic formulation of Grothendieck's definition of (bi)fibration, and extend this to a definition of_monoidal closed bifibrations_, which we see as a natural space in which to study the properties of proofs and programs. Our main result is a representation theorem for strong monads on a monoidal closed fibration, describing sufficient conditions for a monad to be isomorphic to a continuations monad "up to pullback".
Keywords
Cite
@article{arxiv.1310.0263,
title = {Type refinement and monoidal closed bifibrations},
author = {Paul-André Melliès and Noam Zeilberger},
journal= {arXiv preprint arXiv:1310.0263},
year = {2013}
}