By size, I mean the universe inhabited by the motive of the induction. binPeano quantifies over the motive inside the induction, so elimination over Set(n+1) is required to justify elimination over Set(n). Meanwhile, the Peano family is just an ordinary Set, and it does for all.

I guess I’d also observe that binPeano is a higher-order function full of continuation-passing voodoo, whilst peano and its little friend are first order. Some people love that higher-order stuff, and finality in general, because you can do anything, but I love initiality, because it enables me to see everything.

Can you elaborate on this? What is expensive, and how are you measuring the size of inductions?

I find it a little unfair that peano got a helper function, but binPeano has to do all the work itself. More fair would be to say

binPeano (b;1) P p1 ps := ps (binPeano (b;0) P p1 ps)

Of course the body of binPeano (b;0) would have to be given it’s own name (binDouble) to make this properly structurally recursive.

jag, you’re absolutely right; I’ve fixed it.

Russell, Epigram 2′s core theory has the restricted kind of inductive families you get in Agda 1, where constructors must target the full range of indices. You’re right, with that alone you can’t define Peano. However, unlike Agda 1, we also have a propositional equality, and that allows us to simulate full inductive families in a uniform way by adding “Ford equations”. So, in this example, we won’t say “p1 returns Peano 1″, but we will say “p1 returns Peano b for any b you like as long as it’s equal to 1″. In the source language, we’ll sugar away the explicit equation mangling (much as we currently do), so it looks pretty much the way it does now.

bsuc (b; 1) = bsuc b; 0

?