Dependent Inductive and Coinductive Types are Fibrational Dialgebras

TL;DR

This paper develops a categorical framework using fibrations to interpret dependent inductive and coinductive types, proposing a unified view as dialgebras and extending the understanding of dependent data types in type theories.

Contribution

It introduces a class of functors on fibrations and demonstrates how dependent inductive and coinductive types correspond to initial and final dialgebras, respectively, providing a new perspective on their treatment in type theories.

Findings

Dependent types are modeled as dialgebras in a fibrational setting.

Coinductive types are treated as duals of inductive types within this framework.

The approach connects dependent data types to dependent polynomial functors.

Abstract

In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories \`a la Martin-L\"of can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors. This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.