Check strict positivity of datatypes

[jespercockx]

Currently we do not check positivity in any way, we should actually check that the datatypes we define are strictly positive (see also #29). However, we should be careful to not be too restrictive: Agda has a broad range of datatypes that it recognizes as strictly positive. Hence it might make sense to add some extra judgements for proving that a certain function or type is strictly positive in one of its arguments.