indexing in definition of "code"

[DanGrayson]

Dan L should check whether my fix to the definition of "code" in f8530d9 is okay (if it's his definition), and whether it prompts any modification to the proofs.

[favonia]

This is exactly how I formalized the proof in Agda. Yes, you want a separate constructor (in terms of type theory) for n=0.

[mikeshulman]

Oh man, you confused me into not looking at this by blaming Dan L for it. I'm the one who wrote the van Kampen section. Yeah, that's more correct. I kind of feel like it should be possible to define things so that n=0 isn't a special case, but maybe that doesn't work with the way you Agda'ed it.