A generalization of positive inductive and coinductive types to
monotone inductive and coinductive constructors of rank 1 and rank 2
is described. The motivation is taken from initial algebras and final
coalgebras in a functor category and the Curry-Howard-correspondence.
The definition of the system as a lambda-calculus requires an
appropriate definition of monotonicity to overcome subtle problems,
most notably to ensure that the (co-)inductive constructors introduced
via monotonicity of the underlying constructor of rank 2 are also
monotone as constructors of rank 1. The problem is solved, strong
normalization shown, and the notion proven to be wide enough to cover
even highly pathological examples.
