Skip to main content

Questions tagged [positivity]

Positivity is a common restriction when defining inductive types in type-theory based proof assistants.

Filter by
Sorted by
Tagged with
1 vote
0 answers

Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?

Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
15 votes
1 answer

What are the complex induction patterns supported by Agda?

A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
5 votes
0 answers

What are the conditions for Agda to detect that induction-recursion has a least fixed point?

This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype. The idea (rephrased): ...
7 votes
2 answers

Proving strict positivity in Agda

In Agda we can prove termination of functions by using well-founded relations, is there a guideline for proving datatype declarations strictly positive, possibly via use of some container techniques ...
3 votes
1 answer

Can you remove strict positivity from mere propositions?

You can encode induction impredicatively. Some minimalist theories dispense entirely with inductive/coinductive types for proof irrelevant impredicative sorts. But in a practical theorem prover it's ...
10 votes
2 answers

Replacing (strict) positivity with monotonicity on propositions

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to ...