[[!redirects inductive recursive type]] [PDF of Peter Dybjer's 2000 paper on inductive-recursive types](http://www.cse.chalmers.se/~peterd/papers/Inductive_Recursive.pdf) As at 9 June 2014, [[Agda]] supports induction-recursion, but [[Coq]] does not.