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
7 votes
2 answers
292 views

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 ...
Ilk's user avatar
  • 547
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 ...
Meven Lennon-Bertrand's user avatar
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 ...
Trebor's user avatar
  • 4,025