The abstract from the article:

"It is sometimes convenient or useful in mathematics to treat isomorphic structures as
the same. The recently proposed Univalence Axiom for the foundations of mathematics
elevates this idea to a foundational principle in the setting of Homotopy Type Theory [HTT]
It states, roughly, that isomorphic structures can be identified. We explore the motivations and consequences, both mathematical and philosophical, of making such a new
logical postulate."

By "isomorphic" I understand "similar to a desired and useful degree." Perhaps you can clarify what it means to say that "isomorphic structures can be identified." What is "identified"?

And a sentence or two on what HTT is, and why it adds anything to elevate a standard practice (treating isomorphic structures the same - in certain significant ways) to a foundational principle. In other words, what's the big deal - is there any "deal" at all, and why does it matter?

I'm thinking you can limn all this in a relatively few words, at least to get the slow among us - me - up to speed.

One point that I found enlightening was the suggestion that, to paraphrase, invariance under homotopy equivalence is a hallmark of logicality. — RainyDay

I don't agree on this point. Of course you can define "logicality" however you want, but in my opinion HoTT without Univalence Axiom has all rights to be regarded as "real" logic as HoTT without Univalence, or ZF Set theory in first order logic.
The point is that the "natural" model of HoTT without UA is not the usual mathematical universe that mathematicians have in mind, but a much wider one. For example, function extensionality is not derivable. That's because the "functions" described by HoTT without UA contain information on how they are executed, and not only the relation between input and output values. So, wihtout HoTT, two functions can be different because they have different "implementations", even having the same input-output correnpondence. The same is true for isomorphic structures: I think there are alternative axioms not compatible with UA that describe perfectly reasonable mathematical models where isomorphic structures should NOT be identified, just at the same way as there are perfectly reasonable mathematical models where the law of excluded middle should be assumed to be FALSE (for example, if you consider the possibility of partial functions).
The remarcable characteristic of HoTT with UA is that it's "natural" model is the same model assumed by category theory.

If I had to choose a characteristic of pure "logicality" (e.g. a caracteristic of all logics), I would rather say that it's related only to computability and finiteness of execution.

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.

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

I'm probably having trouble separating HoTT+UA from HoTT. Doesn't truncation allow us to ignore identifications where necessary anyway? — RainyDay

Well, for HoTT without UA I had in mind Coq with higher inductive types (https://ncatlab.org/nlab/show/higher+inductive+type).
Well, you can use truncation to identify proofs ( objects of type "Prop" in Coq ), but we don't want to identify functions ( objects of type "Set" in Coq ). Identifying proofs of equality on functions does not prevent you to build different functions with the same input-output relation.

Is there an example you had in mind where we'd not want isomorphic structures identified and also not want UA? — RainyDay

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.
However, I believe it's still possible to have both an "Univalence" type where UA is assumed to be true, used to reason about extensional functions, and a "Set" type where UA is assumed to be false, used to reason about programs.

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.

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

Is the UA intended to apply to standard set theory? In other words in the category of sets, a morphism is a bijection. If isomorphism is identity, then there is exactly one set of each cardinality. This is actually a very helpful point of view sometimes. For example the set of natural numbers and the set of rational numbers are exactly the same set. All we've done is named its elements in two different ways. That's my set-theoretic understanding of "isomorphism is identity."

Another common example is, say, the group of integers mod 4. This group is isomorphic to the set {1, i, -1, i} of complex numbers, with the operation of multiplication. These are two different groups, but they are isomorphic to each other. This is something students of abstract algebra come to understand at some point. That we can mentally identify the two groups as if they were the same group.

On the other hand there might be applications in which we do want to remember that these are two distinct groups that happen to be isomorphic. From the traditional (non-UA) point of view, we say that there is only one cyclic group of order 4; but when pressed, we admit that it shows up in many different disguises that are set-theoretically distinct.

Is this how I should be approaching trying to understand the UA?

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?

Is the UA intended to apply to standard set theory? — fishfry

Here's a quote from the introduction of Univalence as a Principle of Logic
"The resulting picture of the mathematical universe is rather different from that
corresponding to conventional set theoretic foundations"

UA is intended to apply to category theory. If you use standard set theory, two objects of a category can be defferent but isomorphic. So, for example, to be formally correct you shouldn't be allowed to consider THE initial object of a category, because is not unique. But in category theory you are not interested in equality between sets, but only in equality "up to isomorphism".
Well, in HoTT ( and in Coq ) objects are not sets but types. And usually equality between types IS NOT DEFINED: you define only equality between elements of the same type. So, type theory is a more "natural" logic for category theory, because the concept of equality between objects, that doesn't make sense in category theory, IS NOT EXPRESSIBLE.
UA is a way to give a meaning to equality between types (and even to higher order types: types whose elements are types of a lower level) in terms of equivalence relations.

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

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.

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

Yes, of course you can model algorithms and even non total functions in HoTT with UA. In reality you can model it even using Church's untyped lambda calculus, or even using only integer arithmetic (using Godel encoding).
The point is that the objects that correspond "directly" ( without any encoding ) to the axiomatization of HoTT with UA are not algorithms, but standard mathematical functions. And that makes the use of this logic for standard mathematics very convenient, but less convenient (more complex constructions and proofs) for describing algorithms.
At the same way, ZF Set theory's objects are sets (described axiomatically), but you can use sets to build models of whatever you want. Only that the representation of a category (or even operations on natural numbers) by means of sets becomes extremely complex.

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

Ok I can't comment on type theory at all because I'm totally ignorant in that area.

But I'm a little confused by this paragraph. 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.

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.

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.

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?

And what can you mean in the first place by denying that these are objects in the category of groups? Maybe I know a lot less than I think I do. Which is quite possible. But I know what a categorical isomorphism is, and it requires that there are objects that are isomorphic. So I am pretty lost in your paragraph.

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

Yes, this is true for the category of groups built on top of ZF Set theory. You take sets as objects and functions as morphisms. So you have an infinite set of objects that represent the cyclic group of order 4, all isomorphic between each-other.

This is what is called a "concrete category":
"a category that is equipped with a faithful functor to the category of sets" (https://en.wikipedia.org/wiki/Concrete_category).

So, what gives you the possibility to distinguish between the different implementations of the group is a functor, that maps every object to a set built using your underlying set theory (in this case ZF Set theory)

But category theory can even be used as an axiomatic system, independent of ZF Set theory. So, from this point of view, objects and morphisms are "whatever" respects the axioms of a category.
Now, the axioms of category theory require the existence of an "=" relation between morphisms, but they DON'T REQUIRE the existence of an "=" relation between objects.

Now, if you describe a category in a NON CONCRETE way, by giving additional axioms on top of the basic ones (for example existence of all products, existence of limits, etc..) such as is done in the definition of a topos (one of the fundamental structures of homotopy theory), there is no meaning in saying that two objects are equal, simply because NO WAY OF COMPARING TWO OBJECTS IS DEFINED.

So, you can provide an equivalent description of the same two concrete constructions: "the group of integers mod 4 and the powers of i" by building two functors that map objects of the category of groups to their concrete realization as sets.

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

Everything depends on what logic is based your definition of category.
If you take HoTT with UA as your logic, and define the of integers mod 4 and the group of the powers of i as two different types of level 2 (the "Type" type in Coq), then you can build an equivalence relation between the two types and use it in UA to prove that the two objects are equal.
The fact that they are equal means that you can substitute any occurrence of one type with an occurrence of the other type in any proposition. Does this mean that they are "the same" object? Well, I don't know... It means basically that they can be "used" as if they were the same without causing logical inconsistencies.

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

Let's say that they are not "group objects" in the axiomatic interpretation of categories (https://en.wikipedia.org/wiki/Group_object), but are objects in the concrete category of groups, corresponding to a functor in the axiomatic interpretation.

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

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

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

I know that in Coq finiteness of computable functions is ensured by restricting the form of allowed recursive functions, but there are a lot of different ways to achieve the same.

If we stick with computability as logicality, aren't we excluding non-computable statements from being logical? — RainyDay

The restriction to computability is only for set of the procedures and functions used in proofs, not for the functions of the mathematical models

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

Re-reading your post, I realize that maybe I didn't understand what you were referring to...
I didn't see Cornor McBride's talks on linear logic.
Regarding the proposal to "incorporate implementation details into our types" and then distinguish algorithms by "adding some marker element", I don't think it can be done in this way. Types are really only pre and post conditions, and I don't see how you can describe an implementation as function type.

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 understood pretty much everything you wrote. I know what a group object is (as of this morning) by looking it up in Awodey's most excellent book on category theory, which I've been lazily working through (ie "glancing at") for a while now.

So your functor remark was only referring to the forgetful functor that maps a module or vector space to its additive group? Am I understanding that correctly?

I didn't see Cornor McBride's talks on linear logic. — Mephist

What's really interesting are Conor McGregor's talks on linear logic.

Yes, that's what I had in mind, although re-reading what I wrote, I am not sure that this is the right functor to consider.. :razz:

OK, thanks for the suggestion. I'll read it

(It was a joke, really--look up who Conor McGregor is if you're not familiar with him)

Ah... well, I don't know neither MgGregor, nor McBride or linear logic.. :smile:

↪Terrapin Station OK, thanks for the suggestion. I'll read it — Mephist

LOL Now I don't feel so bad about my own ignorance of weighty matters!

Re the functor that cranks out groups ... I recalled and just looked up the fact that in some categories the forgetful functor Grp -> Set has a left adjoint which is the free functor; namely the functor that inputs a set and outputs a free object on it, such as for example the construction of a free group on a set. Could that be what you were thinking of earlier?

I tried to look for the "standard" encoding of category theory in HoTT, but it seems that there are many, and none is standard (same thing as in set theory...). Anyway, the one chosen in the HoTT book is not what I said: objects are not types, but there is a type whose elements are the objects of the category.

Anyway, the idea of representing groups with functors is very simple:
first of all, since isomorphisms are equivalence relations, UA implies that isomorphic groups are equal. So, as you said, in the category of groups there is only one object representing the cyclic group of order 4.
But of course you can build objects that have the structure of a group (group objects) in any cartesian closed category: for example you can define natural and complex numbers in the usual way on the category of sets (surely in HoTT there are many much more efficient representations of natural and real numbers than this one but, as long as you can prove that they are isomorphic, the one that you choose is only a matter or convenience).
So a representation of the category of groups with sets is a functor from Groups to Sets. And of course there are many different representations of the same group as sets, corresponding to many different functors from groups to sets.

(https://ncatlab.org/nlab/show/representation):
"3. General definition
In a rather general form, we therefore have a representation of a category C in a category D is simply a functor F:C→D."

Anyway, the idea of representing groups with functors is very simple — Mephist

Ah, group representations on steroids. I understand at least by analogy. The ncatlab link you provided was extremely helpful, thanks. Also the Wiki article on group objects is very good in case anyone else is trying to claw their way up this abstract area of math.

I had a little insight. I read another Awodey paper, Structuralism, Invariance, and Univalence and it snapped everything into focus.

UA is the statement that "Isomorphic objects are identical."

In standard (set-theoretic) math, UA is a sort of folklore viewpoint. Everyone regards isomorphic objects as the same, even though we secretly know that they are different sets. We agree to ignore this little defect in set theory.

As Awodey puts it:

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.

I internalized this idea a long time ago, and have been puzzled at what is the point of restating it in the context of HOTT.

The point is that HOTT allows us make the folklore viewpoint exact.

In HOTT we can express the idea that "Isomorphic objects are identical" as a precise mathematical statement. HOTT clarifies all the muddled conceptual areas that arise when we try to nail down how two different things are the same by virtue of sharing all of the "appropriate structural properties." What's a property? How do we know which ones matter to our structure? What's a structure? HOTT makes mathematically precise what was formerly vague. That's my latest understanding.

"HOTT makes UA legit" is the insight I've been looking for.