Steve Awodey
Steve Awodey
We could reduce possible confusion by referring back to Lemma 6.25, and recall the issues by writing (more correctly): f(base) :== b ap_f(loop) := L
MS: "The book doesn't reserve "proposition" to refer to only (-1)-types; it calls those "mere propositions"." good point! I think a compromise also determined that it's ok to simply display...
true. But the convention (I guess) is that simply displaying a type such as a = b means the same as the judgement that the type is inhabited (or rather,...
that in response to MS: "There is a bit of lack of parallelism in these sentences of the form "such that P and Q" where P is a judgment and...
agreed.
Why isn't that just what that paragraph already explains?
How about this:we canobtain such represen-tatives in a natural way by truncating the universe.Steve On Jun 14, 2024, at 18:24, Mike Shulman ***@***.***> wrote: James Hanson has pointed out that...
I think comparisons with previous authors, such as Bishop and Troelstra-vanDalen, are more persuasive than appeals to what someone thinks is “standard” or “horrible”.
I would certainly avoid using b:A, since b:B is already mentioned in the definition. there are enough other letters available ... : - )
I think this would be too big a change. Moreover there are probably authors of the book who would not agree.