Advisor: Steven Schäfer
Strictly positive type expressions can be used to describe many interesting types, in particular nested inductive and coinductive ones. My goal is to show that the corresponding types exist and that they are unique. For this purpose, I study containers as a normal form representing the functors that correspond to strictly positive type expressions with free variables. I prove that containers are closed under operations like product and fixed points and formalized a construction of coinductive types from natural numbers.