Type Theory based on Dependent Inductive and Coinductive Types

Henning Basold, Herman Geuvers

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theor…