Andrej Bauer

And in fact, _all_ definitions are equivalence preserving.

Right. If we manage to push it through _everything_ then how close are we to a computational interpretation of univalence?

Lulu can give us an ISBN. Or maybe IAS.

Maybe this is where IAS can do its share?

I see, well then the most straightforward option is to buy an ISBN from Lulu. That may land us a LOC entry too.

I dunno, read the docs.

You mean, is there someone listening who knows how to do this?

Suppose A and B are truth values (ooo, I like the new terminology for h-propositions) and we want to say A + B. Then it sounds strange, for instance "there...

I don't like "proof" for the same reason I dislike "propostion". It makes people think of syntax too much. Whatever phrase we use, it has to be flexible. Choice is...

Actually, we should have a second-edition milestone.