Typos in proof of Lemma 10.3.12

[LuuBluum]

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.

[mikeshulman]

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?

[LuuBluum]

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).

[mikeshulman]

Yes, that does seem to be true. It's a bit surprising.

Would you like to submit a pull request?

[awodey]

I would certainly avoid using b:A, since b:B is already mentioned in the definition. there are enough other letters available ...
: - )

[LuuBluum]

I can make a PR, though it might be a little bit before I can get around to it.