Skip to content

Constructing Simple and Mutual Inductive Types in Agda.

Notifications You must be signed in to change notification settings

stefaniatadama/inductive_types

Repository files navigation

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.

About

Constructing Simple and Mutual Inductive Types in Agda.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages