Philosophy behind monotonicity requirement for inductive types Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions?  According to my understanding of the Bishop/Martin-Löf view of mathematics, to construct a set is to say how to construct elements of said set (as well as say how elements are identified, but that's not so important for this discussion).  That's fine, but then I don't see why the standard inductive presentation of the naturals is a valid construction, but something like

Inductive bad :=
  | b : (bad -&gt; bad) -&gt; bad.


is not.  To be clear, I understand how such definitions yield inconsistencies and so I certainly understand from a purely pragmatic perspective why such restrictions need to be made.   However, it's one thing to be able to banish inconsistency, and another to be able to give a natural explanation for why such restrictions should be made.
When you write an inductive, you are defining a type by an equation. For example, if we write $F_1(X)=X^X=X\to X$, bad should satisfy $F_1($bad$)=$bad.

In general such equations can have several solutions, or none. For example, for $F_2(X)=X^X\times X$, you have (at least) two distinct solutions: $0$ (empty set) and $1$ (singleton). So you want some way to pick a specific solution.

The fact that you declared your type as inductive means that you pick the smallest solution (and coinductive would've meant the largest). So you want to be sure that this smallest solution exists. One way to ensure this is to ask for $F$ to be monotonous because then, the Knaster–Tarski theorem implies that it has a smallest fixpoint.

Aside from inconsistencies, I don't see a reason to ban other classes of equations, as long as you have a way to pick a specific solution. But unless you are sure that there is always a smallest solution for those equations, and that you will pick it, you probably shouldn't call it inductive.