positivity condition in Coq/CIC

Question

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?