Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals? Coq lets you define an inductive type of the following form:
Inductive Foo :=
  | Base : Foo
  | Positive : (nat -> Foo) -> Foo.

because the position of Foo in the premise of the Positive constructor is considered by Coq to be a positive position.
Coq rejects an inductive definition where the type being defined appears in a negative position in a premise. Accepting such a definition would enable the construction of non-normalizing terms. In particular, it is not possible to create an induction principle for such a definition.
For example:
Inductive SnaFoo :=
  | Negative : (SnaFoo -> nat) -> SnaFoo.

is rejected with the error message:
Error: Non strictly positive occurrence of "SnaFoo" in "((SnaFoo -> nat) -> nat) -> SnaFoo".

But Coq also rejects the following definition:
Inductive Bar :=
  | IsItPositive : ((Bar -> nat) -> nat) -> Bar.

The position of Bar in the premise of the IsItPositive constructor is not obviously positive but I have seen a presentation (sorry, I can no longer find the link) that accepted this position as positive. I could formulate a plausible inductive principle for Bar as follows:
Definition Bar_ind (P : Bar -> Prop) :=
  (forall (F : (Bar -> nat) -> nat),
    (forall f g, (forall (b : Bar), P b -> f b = g b) -> F f = F g)
    -> P (IsItPositive F))
  -> forall (b : Bar), P b.

More importantly, assuming the existence of enough inaccessible cardinals, I think I can prove that there is a model of Coq's type theory that contains inductive types like Bar, with the inductive principle that I proposed. I did prove that the presence of $\omega^2$ inaccessibles is enough to accommodate Bar itself, assuming that all the other inductive types in the model conform to Coq's positivity rules. I don't know how many inaccessibles will be required to relax the positivity assumptions of Coq in general.
My question is twofold:
First, what is the reason that Coq does not admit definitions like Bar?
Second, what is a good reference for the topic of admissibility of inductive types?
 A: Assuming classical definite description there is a function
decide : forall {A : Prop} (P : A -> Prop), A -> nat

s.t.
(decide P x = 1 <-> P x) /\ (decide P x = 0 <-> ~ P x)

It follows under the assumption of propositional extensionality that, moreover
forall A (P Q : Q -> Prop), decide P = decide Q <-> (forall x, P x = Q x)


Thus, we would have
Definition contains_power (P : Bar -> Prop) : Bar := IsItPositive (fun x => decide P x).

Which would be injective.
As such, your type includes its own power set, which violates Cantor's theorem. For a more detailed account of the argument where Prop replaces nat, see https://coq.inria.fr/refman/language/core/inductive.html in the paragraph "it is less obvious why"
I know not how much of the classical argument here is needed to produce a contradiction, but it seems to me unlikely that there is a sets-and-functions model which has your Bar type in it (assuming, at least, that what ever large cardinals you need are consistent). But, I could imagine that there might be an alternative model, however, that exploits some of the constructive structure of the type theory--maybe this is what you have cooked up?
