Where do we rely on the boudned nesting of constructors

[andrejbauer]

Somewhere in the proof we presumably rely on the fact that there is a bound on how deeply the point constructors are nested in the path constructors. Where? (I do not mean the n in the definition of H_Con^n, I mean where do we need the fact that there is such an n?)

[nmvdw]

We use this assumption in Lemma 10. We need it, because otherwise we make a map from the constructor terms. We refer to lemma 11 on page 6 in 'From Lemma 10 ...'.

[andrejbauer]

I don't think that's the place. Lemma 10 is about a single constructor term, and so obviously it's going to have an n. Somewhere we need to know that all the constructor terms have a common bound to nesting of constructors.

[nmvdw]

But we need to apply Lemma 10 to every constructor term, because for all constructor terms we need the induced map. On page 6 we apply Lemma 10 to every constructor term to get the maps, and because there is a maximum, we can map them all in H_Con^n.

[andrejbauer]

As I said at the beginning, I am asking where else we need to know this, other than H_Conn^n. Somewhere it should show up, or else it ought to be possible to consider the unbounded case by creating a longer sequence in the colimit. In any case, it's not very important.