2015/08/31 by Henning Basold
Computer Science · Mathematics · #Algebra over a field #Categorical variable #Class (philosophy) #Coinduction #Computability, Logic, AI Algorithms #Functor #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems #Type (biology) #Type theory #cs.LO
paper · pdf · doi:10.4204/eptcs.191.3
published in Electronic Proceedings in Theoretical Computer Science 191, 3-17 (Open Publishing Association) · In Proceedings FICS 2015, arXiv:1509.02826
openalex publication_date 2015/09/09 · arxiv created 2015/09/10 · arxiv updated 2016/02/22 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/06
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.