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) (decide P x = 1 P x) /\ (decide P x = 0 ~ P x) Second, what is a good reference for the topic of admissibility of inductive types?Īssuming classical definite description there is a function decide : forall (P : A -> Prop), A -> nat I don't know how many inaccessibles will be required to relax the positivity assumptions of Coq in general.įirst, what is the reason that Coq does not admit definitions like Bar? 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. 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. (forall f g, (forall (b : Bar), P b -> f b = g b) -> F f = F g) I could formulate a plausible inductive principle for Bar as follows: Definition Bar_ind (P : Bar -> Prop) :=
![coq definition coq definition](https://cafedelites.com/wp-content/uploads/2018/11/Coq-Au-Vin-IMAGE-13.jpg)
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. | IsItPositive : ((Bar -> nat) -> nat) -> Bar. Is rejected with the error message: Error: Non strictly positive occurrence of "SnaFoo" in "((SnaFoo -> nat) -> nat) -> SnaFoo".īut Coq also rejects the following definition: Inductive Bar := In particular, it is not possible to create an induction principle for such a definition. Accepting such a definition would enable the construction of non-normalizing terms. Coq lets you define an inductive type of the following form: Inductive Foo :=īecause the position of Foo in the premise of the Positive constructor is considered by Coq to be a positive position.Ĭoq rejects an inductive definition where the type being defined appears in a negative position in a premise.