  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".
