HoTT
Typos in proof of Lemma 10.3.12
The proof, alongside the relevant definition:
The issue here is that there seems to be a significant amount of overloading of both a and b here, so that it's not really clear what's happening at all with the types. Especially in the sentence, "the inductive hypothesis for a : A says that for any a' < a, and any b : B, if f(a') = f(b) then a = b." Shouldn't that be b : A? The whole thing is rather muddled as a result.
Additionally, on working out this proof in Agda, this doesn't even take double induction. The first induction is enough; the dual argument still uses that first induction but instead of relying on the assumed c < a, it relies on the fact that you managed to construct c' < a.
Yes, that should be b:A in that sentence. With that change, I think the proof is correct; all the variables in it range only over elements of A. It's true that in the definition, b ranges over elements of B instead, but I don't know if that's a serious problem?
Yeah, that part is fine, though I think it would also be cleaner if the double-induction part is removed since it's entirely superfluous (you never use that inner induction hypothesis; even in the dual argument, you still use the first hypothesis).
Yes, that does seem to be true. It's a bit surprising.
Would you like to submit a pull request?
I would certainly avoid using b:A, since b:B is already mentioned in the definition. there are enough other letters available ... : - )
I can make a PR, though it might be a little bit before I can get around to it.