All Questions
Tagged with inductive-type positivity
4
questions
1
vote
0
answers
63
views
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 ...
- 143
18
votes
1
answer
1k
views
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,510
3
votes
1
answer
115
views
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 ...
- 2,868
10
votes
2
answers
547
views
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 ...
- 4,025