The obvious example is the Set type in Coq. Set is not meant to represent mathematical functions, but to represent algorithms (functions that can be "extracted" by the system as programs). If you assume UA for Set, all algorithms that compute the same function are equal, and of course you don't want this to be the case, because different implementations are very different in terms of execution time and memory usage. — Mephist

I thought we'd be able to incorporate implementation details (a description of them at least) into our types and differentiate them at that level followed by a truncation to Set as required for computation. Conor McBride and his talks on linear logic gave me that impression. If the problem is how to distinguish algorithms when reduced to Set, can't we just add some marker element and still retain UA?

I've been trying to read the HoTT book but it's quite the challenge for somebody without a maths degree. Are there any other good resources you'd recommend?

"I think there are alternative axioms not compatible with UA that describe perfectly reasonable mathematical models where isomorphic structures should NOT be identified."

I thought this was interesting. I'm probably having trouble separating HoTT+UA from HoTT. Doesn't truncation allow us to ignore identifications where necessary anyway? Is there an example you had in mind where we'd not want isomorphic structures identified and also not want UA?

I'll have to think more on your reply so thank you for that. I suspect you know far more than I about all this. Yet you still took my bait about logicality. I don't care what's logical really. I just want people talking about HoTT. ;)

Edit: No, I can't say that. I do care. Is there a formal way to express finiteness of execution? I presume you mean finite in principle. If we stick with computability as logicality, aren't we excluding non-computable statements from being logical? I see the appeal but it also seems to unnecessarily conflate two perfectly good concepts.

First of all, thank you for replying to such a daunting topic. I think if more philosophers stuck their nose into mathematics, both fields would benefit.


Identification is a kind of pairing of two things. We identify one with the other. Isomorphisms describe how we go between the two things. Consider a sheet of paper. We could curl one side around to its opposite edge and 'identify' the two edges. Now we've got a cylinder. Another identification of the same two edges would be to twist the paper as we curl it and, voila, Mobius strip.

Some theories have a bit of trouble (formally, at least) with identification because they consider two things to be equal just when their extent is equal. Two sets for example are equal iff they contain the same elements. The trouble comes in because, although two sets may be isomorphic (we have some idea of how to move between them), set theory can't identify the two because they contain different elements. Most mathematicians tend to ignore this I believe but HoTT and, similar theories, provide a way to formally identify isomorphic structures. It may seem like a technicality but getting this sorted out has advantages in making proofs and mathematics in general more computable.

This isn't a complete answer but I hope it clarifies more than it confuses.

@Jake

I wouldn't say "calmly bored" but your experience may differ. As for useful and important, I gave two examples. Understanding others and understanding our own mortality. Or perhaps politics, another rich area of philosophy, could help you persuade the masses to care.

I expect you won't be satisfied with philosophy though unless it immediately address your concern about nuclear weapons.

If you literally had a gun in your mouth, I'd be intrigued. I don't necessarily consider suicidal people nuts though and, yeah, I can imagine numerous reasons you wouldn't want to discuss it. After that acceptance of death I spoke about, discussions on how to avoid it etc become extremely dull.

Philosophy might help you understand why others don't share your concern. Ethics, in particular, and the disagreement over what one ought do. You seem to have a pretty sure idea of what we all should be doing but many of us have learned to live with the metaphorical gun in our mouths in different ways.

Once you've accepted that life, all life perhaps, could end in an instant, your own life kind of starts anew. That's a shift of perspective I don't think you want but it's one small part of why philosophy is more than a "clever parlor game".

Some games require mixed strategies for pareto optimality. If such games exist in whatever context ethics is considered, then ethical theories which only proscribe pure strategies couldn't suffice.

Categorical imperatives ala Kant, for example, seem like the ethical version of a pure strategy. I suspect ethical language is flexible enough though to equivocate between 'pure' and 'mixed' strategies.

Congratulations (almost) everyone for keeping a cool head through 25 pages. I wonder if acceptance/rejection of the principal of indifference (https://en.wikipedia.org/wiki/Principle_of_indifference) is what divides many people.

I'd also like to see the original problem rephrased to eliminate personal valuations of the outcome. There's little value in the question if we can all argue along lines of "oh well, I always switch 'cause I'm curious" or "after I see the first amount, I already feel like a winner and that's enough for me".