In this project, we have introduced a general datatype which lets you define any simply typed, strictly positive inductive type as an instance of it. A primitive recursion for that type can then be automatically constructed, allowing you to define simple types and operations over them in a minimal system.