One point that I found enlightening was the suggestion that, to paraphrase, invariance under homotopy equivalence is a hallmark of logicality. — RainyDay
I'm probably having trouble separating HoTT+UA from HoTT. Doesn't truncation allow us to ignore identifications where necessary anyway? — RainyDay
Is there an example you had in mind where we'd not want isomorphic structures identified and also not want UA? — RainyDay
P.S. Isomorphic structures to be equal in Set would mean that you don't distinguish between different implementations of the same algebraic data structure. This is good for mathematics but not for programming. — Mephist
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
Is the UA intended to apply to standard set theory? — fishfry
Now if I imagine that there is exactly one set of each cardinality; and that the group of integers mod 4 and the powers of i are the same group (and not just two isomorphic groups) is that in the spirit of UA? Is this a simplified way of understanding it? — fishfry
I thought we'd be able to incorporate implementation details 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? — RainyDay
The group of integers mod 4 and the powers of i are not objects in the category of groups, but functors from categories with the appropriate structure of morphisms to the category of groups. You can still use functors to build whatever structure you want, and in the category of functors, these structures are no more isomorphic. — Mephist
I would have thought -- in fact I do think -- that each of these groups is an object in the category of groups; and that there are morphisms from one to the other and back whose compositions are the respective identities, hence the two groups are isomorphic. This is true in category theory. — fishfry
I would think that UA simply says that from now on I should just think of there being one group, the cyclic group of order 4, and I shouldn't care that there are two different set-theoretic presentations of it. Which is how we normally think of it anyway. Which is how I'm approaching UA. — fishfry
But your para is quite opaque to me. You say the integers mod 4 and the powers of i are NOT objects in the category of groups. I'm in deep trouble here, please throw me a lifeline. — fishfry
But to see them as functors, I'm not sure I get that. Functors from "categories with the appropriate structure of morphisms to the category of groups." Ayyy. I'm in trouble. Help me out please.
What are the categories with the appropriate structure etc.? Can you give me an example? — fishfry
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 — RainyDay
If we stick with computability as logicality, aren't we excluding non-computable statements from being logical? — RainyDay
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? — RainyDay
The category of modules (https://en.wikipedia.org/wiki/Category_of_modules)
and the category of vector spaces (https://ncatlab.org/nlab/show/Vect) for complex numbers — Mephist
I didn't see Cornor McBride's talks on linear logic. — Mephist
↪Terrapin Station OK, thanks for the suggestion. I'll read it — Mephist
Anyway, the idea of representing groups with functors is very simple — Mephist
This common practice is even sometimes referred to light-heartedly as “abuse of notation,” and mathematicians have developed a sort of systematic sloppiness to help them implement this principle, which is quite useful in practice, despite being literally false. It is, namely, incompatible with conventional foundations of mathematics in set theory.
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.