/inductive_types

Constructing Simple and Mutual Inductive Types in Agda.

Primary LanguageAgda

inductive_types

Martin-Löf's dependent type theory is a formal language developed on the principles of constructive mathematics. It acts as the basis for modern proof assistants like Agda, which are tools for doing computer-assisted mathematics. This dissertation investigates the central notion of an inductive type within Martin-Löf type theory. We construct a small theory of signatures as a framework in which we can express simple or mutual inductive types. For a given signature, we then construct algebras, algebra morphisms, the initial algebra, and a unique morphism from the initial algebra to any other algebra called the iterator. We thus obtain a complete specification of simple and mutual inductive types. Next, we focus on the W-type, an inductive type which encapsulates the recursive aspect of any inductive type. For a given signature, we construct an algebra for the indexed W-type's representation of the signature. We then present our attempt at constructing the iterator for this algebra. This provides a starting point for completing a reduction from simple and mutual inductive types to W-types, in order to show that a type theory supporting W-types can support all simple and mutual inductive types.