Altenkirch et al. present a method to construct strictly positive families of types in extensional type theory. To this end, they use the notion of containers (also known as polynomial functors) as a normal form for functors between families and show that the class of functors with such a normal form is closed under strictly positive type formers like product, coproduct and most notably inductive and coinductive fixed points.
In my bachelors thesis, I demonstrated that this does also work in homotopy type theory but only for the construction of strictly positive types instead of families. Moreover, I developed a construction of W-types from the type of natural numbers, which allows us to work in a type theory with a smaller core without any loss in strength.
It turns out that this core is basically the type theory that is used by the Coq-formalization of the UniMath project. At the moment there is no general way to define new types in this formalization because it uses a restricted subset of Coq that does not include the Inductive keyword. The main goal of my research immersion lab is to generalize my work to families of types and to integrate it into the UniMath formalization. If successful, this will offer an easy way to define (co-)inductive types and families. Further goals are the exploration of principles for reasoning about coinductive types and the construction of the rational fixed point of containers which describes eventually periodic data structures.
Fri Mar 2 17:20:08 2018