Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a constructor. This is because if no such condition were made the fixed point combinator could be written and the systems would become inconsistent. Ok great but perhaps this is overly zealous in eliminating these kinds of paths to inconsistency. It reminds me of the the difference between Coq and Agda recursion. Agda allows for recursion in multiple arguments where as Coq requires that one of the arguments always decrease. Is there something similar that we can do with inductive definitions?
Is there a better rule that could be used to allow for more definitions?