positivity condition in Coq/CIC

I am recently learning the theory behind Coq and learnt that positivity condition guarantees termination of the program. But my question is, what would you think of the following definition?

Inductive t : Set := b : t | c : ((t -> unit) -> unit) -> t.

Sure it won't compile in Coq, but would it jeopardize termination guarantee? More precisely, in this definition, t is in a positive position as well, isn't it? So can I say theoretically speaking this should have also been a valid definition? Otherwise do you have any counter example?

My thought is, (t -> unit) -> unit should be isomorphic to t according to Yoneda lemma so it should be pretty safe, isn't it?

The positivity condition is not there just so that "programs terminate", as you put it (what programs?), but to make sure the type is well defined in the first place. The inductive definitions define the smallest type satisfying an equation. That is, we put into the type only those things which are prescribed by the clauses of the definition, and no arbitrary garbage. (Non-normalizing terms count as garbage, and I think that's what you meant when you spoke of terminating programs.)

Let us take a step back and think where the inductive definitions come from. They are solutions to type equations. Here is a type equation:
$$N = \mathtt{unit} + N.$$
What could $N$ be? We might be thinking that it must be the natural numbers, since every element of $N$ is either $\mathtt{inl}(\mathtt{tt})$, which is a fancy way to say "zero", or it is of the form $\mathtt{inr}(n)$ for some $n : N$. But this need not be the case! For example, $N$ could also contain a special element $\infty$ satisfying $\infty = \mathtt{inr}(\infty)$. It could also contain an extra "fake zero" $\mathtt{Z}$, together with its successors $\mathtt{inr}(\mathtt{Z})$, $\mathtt{inr}(\mathtt{inr}(\mathtt{Z}))$, ... There are many solutions to the above equation.

The smallest solution is called the inductive type, and the largest one the coinductive type. I am skipping technicalities about what "smallest" and "largest" mean precisely (they are the "initial algebra" and "final coalgebra", respectively), but I hope you get the point.

In order for us to say that we have a well-defined inductive type, we need to know that the smallest solution to the type equation actually exists. In fact, it does not always exist, sometimes there can be several incomparable solutions, or none at all. The positivity condition in Coq and CIC ensures that a smallest solution exists. It's not the only possible condition one could come up with, and there are variants, but for the purposes of a proof assistant we need something that makes sense computationally, and can actually be verified by a type checker (for instance, it wouldn't do to say that an inductive definition is valid if it defines a $\kappa$-accessible functor for some cardinal $\kappa$, and have the proof checker look for $\kappa$ – hmm, that's an interesting thought).

If we now look at your proposed definition

Inductive t : Type := b : t | c : ((t -> unit) -> unit) -> t.

the question to be asked is: how do you know that the smallest solution exists? Somebody proved that the strict positivity requirement ensures the existence, but your definition falls outside that criterion. You need to provide evidence that there is such a type. The evidence must be a well argued explanation of what the terms of t are that they do not break strong normalization of CIC. You might as well succeed, and there is such a type. The next question then is how do you propose to incorporate your argument into a type checker as a useful algorithm. It's probably not worth the trouble.

Just to show you how problematic these things are, how about the type

Inductive t : Type := c : ((t -> bool) -> bool) -> t.

Is it still totally obvious that there is a smallest solution? We're trying to solve the type equation
$$T = (T \to 2) \to 2.$$
It has no solution in set theory.

StackExchange Computer Science Q#81627, answer score: 6