Skip to main content
23 votes
Accepted

What are the complex induction patterns supported by Agda?

I try to write about what's supported in Agda and the semantics that we have (or don't have) for it. Disclaimers: I'm not an expert on the relevant parts of the Agda source code, I mostly write here ...
András Kovács's user avatar
10 votes
Accepted

Replacing (strict) positivity with monotonicity on propositions

Impredicative strict Prop supports initial F-algebras for all F : Prop → Prop functors. In Coq: ...
András Kovács's user avatar
3 votes

Proving strict positivity in Agda

Are there any techniques that could allow formalizing this argument? Beluga has a notion of 'stratified types' that corresponds to this type of construction. From the user manual: We distinguish ...
gallais's user avatar
  • 1,126
1 vote

Proving strict positivity in Agda

Here's a solution, that I have been making progress with, that fits normal Agda. The aim of defining a type via induction, yet allowing non-obviously decreasing argument in a negative position can be ...
Ilk's user avatar
  • 547
1 vote

Can you remove strict positivity from mere propositions?

If you allow arbitrary fixed points you can inhabit any type. Let $A$ be an arbitrary type. Suppose we had a type $B$ such that $B \cong B \to A$. Then by Lawvere's fixed point theorem $A$ has the ...
Andrej Bauer's user avatar
  • 9,104
1 vote

Replacing (strict) positivity with monotonicity on propositions

Can't you just use an impredicative encoding of inductive datatypes? ...
Ms. Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible