Monotone Recursive Types and Recursive Data Representations in Cedille