Type refinement and monoidal closed bifibrations

TL;DR

This paper explores the concept of type refinement in type theory, linking it to category theory, and introduces monoidal closed bifibrations as a framework for studying proofs and programs, culminating in a representation theorem for strong monads.

Contribution

It establishes a correspondence between type refinement systems and functors, and extends this to define monoidal closed bifibrations, providing a new framework for analyzing proofs and programs.

Findings

Type refinement systems correspond to functors in category theory.

Introduction of monoidal closed bifibrations as a natural setting for proofs and programs.

A representation theorem for strong monads on monoidal closed fibrations.

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