Skip to main content

Questions tagged [induction-recursion]

Induction-recursion allows mutual definition of an inductive type and a recursive function. Induction-recursion is primarily used to inductively define large universes predicatively, thus significantly increasing proof strength of the base theory beyond W-types.

Filter by
Sorted by
Tagged with
5 votes
0 answers
166 views

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): ...
Ilk's user avatar
  • 547