Dependent inductive and coinductive types are fibrational dialgebras

1Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

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 à la Martin-Löf 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.

Cite

CITATION STYLE

APA

Basold, H. (2015). Dependent inductive and coinductive types are fibrational dialgebras. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 191, pp. 3–17). Open Publishing Association. https://doi.org/10.4204/EPTCS.191.3

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free