Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 52 of 52
Univalence identifies isomorphism with identity not by collapsing isomorphism to identity but by expanding identity to coincide with isomorphism. That is, all the isomorphisms (including the automorphisms) are still there, the difference is that now also have just as many equalities.
The type of isomorphisms from to is . The type of automorphisms of is . So an automorphism is the special case of an isomorphism where the two objects are the same.
Univalence says that the type of identities/equalities/identifications between two types and is equivalent to the type of isomorphisms/equivalences between them. This is also true when and are the same, so that is equivalent to . If and are equivalent, then is also equivalent to by composing with that equivalence, and likewise is equivalent to by composing with the corresponding identification. The equivalence then itself passes across univalence to become an identification . But that doesn’t mean that any element of is itself an element of ; you have to explicitly transport it across that identification.
Since this kind of issue is good practice for me, explaining to colleagues, let me butt in. is canonically isomorphic to along .
You have a canonical isomorphism in for all types , using the id construction on p. 26 of the HoTT book. This will correspond to the ’refl’ elements in . For and equivalent (isomorphic) there is no canonical such equivalence.
Mike,
This is also true when and are the same, so that is equivalent to .
Was the final symbol supposed to be ? I
I guess the question is asking what you mean by “same” there.
Was the final symbol supposed to be ?
Yes, fixed, thanks.
I would say that Jrich22’s point is essentially valid. Take for example a connected groupoid . For an object of , we can consider , namely . Now, is equivalent to a groupoid with a single object. In , we have lost the ability to speak about , there is no way to recover it from alone. And if the philosophy is that we should be carrying out constructions which can be carried out equally well in or , then we do not have a good way to speak automorphisms of an object; all objects are on the same footing, because we could choose any of them to pass from to .
This is not to say, of course, that we have lost the ability to speak about Galois theory completely, but it does mean that we have to find a new way to formulate it. This kind of phenomenon is rather fundamental to synthetic homotopy theory.
Sorry, what have we lost? has a single object, say . Then in the type theory, . Or if you prefer to talk from the point of view of category theory, .
Rubbish. Any equivalence induces an isomorphism from . Of course different equivalences will induce different isomorphisms, but that’s not a problem. I think this is JRich22’s misunderstanding too: “treating isomorphic objects as identical” doesn’t mean we forget about which isomorphism gets used to transport from one to the other. By expanding the notion of “equality” to allow two things to be equal in more than one way, univalence enables the resulting equality to remember which equivalence we’re talking about.
In re 10, occasionally people say that groups are equivalent to connected groupoids, but that’s not true. Groups are equivalent to pointed connected groupoids. (Connected groupoids are groups up to conjugacy.)
In reply to #11 and #12: one can speak about the groupoid of automorphisms of , but not itself, i.e. we can know up to isomorphism, but not up to equality, and knowing it up to isomorphism in fact encompasses all isomorphisms in , not only automorphisms of . Yes, of course this is ’not a problem’, indeed it is heart of the matter; this is what I was getting at in my final sentence of #10. I maintain nevertheless that what I wrote in the first paragraph #10 is a valid point of view.
(Let me say as an aside that I am not misunderstanding anything, I was merely attempting to clarify where I think Jrich22’s may be coming from.)
Regarding #13: yes, certainly, the fact that we have to choose an object of was part of the point I was trying to make. There is no canonical choice, and from the univalent point of view any is as good as any other.
No, it is not a valid point of view; Jrich22 was misunderstanding univalence, and if you think he/she had a valid point then you are also misunderstanding. Of course if you care about recovering (or anything else) up to equality, then you aren’t going to be happy with univalence. But recovering it “up to isomorphism” means (here) up to canonical, specified isomorphism, which doesn’t on its own involve anything about other isomorphisms in . There is no need for any change in how we formulate Galois theory: if is a groupoid and then makes perfect sense in univalent homotopy type theory. This should be clear if you read the HoTT book. The fact that any choice of an object in yields an equivalence to a one-object groupoid doesn’t change this.
The choice of an object in together a term of type , no?
@DavidRoberts: Well, it depends on what exactly you want to determine and how. Choosing an object determines a one-object groupoid and a functor that’s fully faithful and essentially surjective, and its inverse equivalence is then determined up to a contractible space of choices.
Sure, good point.
I am not going to continue this discussion, because I am not willing to do so in an atmosphere of dogmatic dismissal. It is a fact that one can use any isomorphism of to replace by an object isomorphic to it, and depending on which choice of in its isomorphism class one is looking at, amongst those arising in this way, the elements are not necessarily automorphisms of in the original sense, they are conjugated with the chosen isomorphism. One has lost the ability to refer to automorphisms of in the original sense. Whether or not one is happy with this, or whether it is technically possible to proceed just as well as we could before, has nothing to do with whether it is a valid point of view. Leaving the discussion here.
Mike, this discussion shows again that it would be more efficient for you and for all future inquirers if answers to these basic questions were collected in an FAQ, such as the stubby “homotopy type theory FAQ” page (or a new version from scratch if that rudiment does not seem worth building on). These same kind of questions have been and will keep coming up.
I’m sorry for being so brusque, Richard, but since there is so much misunderstanding on points like this we simply cannot afford to have people confidently pronouncing erroneous claims like “one has lost the ability to refer to automorphisms in the original sense”. That is just wrong. An automorphism of is defined in the same way it always has been, and still means the same thing. Please learn some HoTT before making statements like that.
Urs, you’re absolutely right; someone just has to find the time…
Unfortunately, I re-opened the discussion thread, and with the greatest reluctance feel the need to give a couple of words of defence. Firstly, I know plenty of HoTT and type theory. Indeed, judging from your n-café posts, I think I may have been aware of it, thinking about it, and programming in Coq, before yourself. However, I form my own opinions and reflections, regardless of whether they follow the mainstream view.
Secondly, you may feel that what I write is wrong, but that is from your point of view, it is not wrong in any objective sense. That the meaning of automorphism has changed is a fact. It makes no difference if one can write down a definition in the same way as before.
I still maintain that what you have said is objectively wrong. I do not understand how something can have changed if it is defined exactly as it was before. The automorphism group of an object of a groupoid does not contain any automorphisms of other objects or isomorphisms between that object and other objects. Transferring across an equality obtained by univalence does exactly the same thing as conjugating by an isomorphism, which has always been something that one can do in a groupoid and doesn’t prevent us from talking about automorphism groups.
The point is the difference between syntactics and semantics. That one can make a definition that is syntactically similar does not imply that it is the same semantically.
I am not saying that one cannot talk about automorphism groups, only that the meaning has changed, and that the original meaning is lost. [Edited to remove something that I realised afterwards is more likely to be confusing than clarifying. May add something later if I find time.]
Found a little time. Maybe the following will help. In univalence, given any construction which we can make with and , we can replace by if and are isomorphic, and replace by something in (its conjugate). This is the elimination rule for identity types. So, for all purposes, is as good as its counterpart in .
But originally may have some meaning in itself (e.g. through the way it was constructed), and I might make a construction which uses that original meaning. For example, we have , viewing the latter as a one-object groupoid. I might take some point on , take some loop at that point, and squash it in so that it becomes an oval. This is meaningless for the which we obtain under the equivalence, if we understand an integer in its usual sense. In univalence, however, a meaning has been given to it. If I tell you to squash an integer to become an oval, you understand this as meaningful. So we lose the original meaning of integers as integers in the usual sense, suddenly they become loops as well, anything under the sun.
This criticism is not so far from those which are sometimes levelled at set theoretic foundations, that it gives formal meaning to things which are not, when we step outside the system, meaningful.
Aren’t you mixing up circle in the two senses?
There’s no problem surely in the former case of identify the fundamental group with . No talk of squashing is possible.
In the latter case, any talk of squashing means you’re thinking of a 0-type with some additional geometric structure, inherited from . This cannot be taken as equivalent to the 1-type, , which has no such extra geometric structure.
Of course, these clever chaps have devised a cohesive HoTT which allows for ’modal’ operators to apply to types, such as , where is your second kind of circle. This is here the fundamental groupoid, yielding a 1-type equivalent to . Of course, ʃ loses all but homotopical information.
I was thinking of as a topological space embedded in , however we define that in HoTT, and as the groupoid whose objects are points of , and whose arrows are paths between them up to homotopy; again, however we define that in HoTT. The arrows are paths embedded in . One should be able, one day at least, to prove in HoTT that in this sense is equivalent to (the proof may use the other definition of , or it may not). The two types and are at the same level; it doesn’t matter what level itself is at, as you essentially point out at the end of your comments.
In univalence, given any construction which we can make with and , we can replace by if and are isomorphic, and replace by something in (its conjugate). This is the elimination rule for identity types. So, for all purposes, is as good as its counterpart in .
This is equally true in classical mathematics: you can always conjugate by an isomorphism to obtain an automorphism of . There is nothing different about univalence here.
I might take some point on , take some loop at that point, and squash it in so that it becomes an oval.
That is not in any foundations a meaningful (nontrivial) construction on automorphisms of a point in , which are homotopy classes of paths in .
This is equally true in classical mathematics
I think you missed the actual point I was making, that in univalent mathematics we can formally replace in any construction and by and the conjugation of . There is no sense in which this is possible in classical mathematics; we do not have an elimination rule in classical mathematics of this kind, we only have an elimination rule for actual equality.
This elimination rule allows us to make sense of constructions on the integers which have no sense classically, e.g. rotating them. Yes, classically we can pass to , rotate, then go back to , but the effect is to do absolutely nothing. We do not have nothing in univalent mathematics, we have made a new construction on the integers, which is meaningless when we step outside the system, according to the intuition as to what an integer is. It may be provably equivalent to doing nothing, but that is immaterial to the point at hand, which is that we have changed the meaning of an integer to encompass the meaning of a loop and many other things.
That is not in any foundations a meaningful (nontrivial) construction
Let’s not waste time nitpicking. Firstly, one can make it perfectly meaningful, e.g. do the same squashing for all loops in the homotopy class. Secondly, it should be sufficient anyhow to illustrate the point.
I think you missed the actual point I was making, that in univalent mathematics we can formally replace in any construction and by and the conjugation of . There is no sense in which this is possible in classical mathematics; we do not have an elimination rule in classical mathematics of this kind, we only have an elimination rule for actual equality.
The point I was making is that any concrete example of such a replacement can also be done in classical mathematics, by simply writing out the application of the isomorphisms by hand. This is essentially the reason why univalence can “compute” e.g. in cubical type theory: it doesn’t actually give you anything new in any concrete instance, the only thing that’s new is the stipulation that it can be done in an arbitrary abstract instance as well.
It’s not nitpicking to point out that “squashing” is the identity map on ; the point is that it’s something that does make sense for as well, since also has an identity map. Univalence does give you a way to transfer an integer to a loop in , do something to that loop (perhaps the identity map), then go back to an integer; but this thing that univalence gives you is equal to something that you could have done already in classical mathematics, so it is not anything new and does not change the “meaning” of an integer.
Let me reorient that a little to help us stick to the point. I don’t want to argue about “the meaning of an integer”. Maybe you could come up with some philosophical notion of “the meaning of an integer” according to which univalence does change it, and I probably wouldn’t agree, but there wouldn’t be any point in arguing about it. What I claim is demonstrably false is a mathematical statement like “we have to find a new way to formulate Galois theory”.
I often encounter a related bemusement:
Are you really saying that all true (mere) propositions and all singleton sets are equal? ’2+2 = 4’ and ’the set of even primes’ are equal!?
What is the best response? There’s something to say about how ’the set of even primes’ is probably being considered as a subtype of the natural numbers, where ’2+2=4’ cannot be. Then there’s something to say about definitional versus propositional equality, just because there is equality in doesn’t mean there is the conceptual relation of definitional equality.
Is there more to say?
The set of all even primes can be considered via the proposition “(n is prime) and (n is even)”, considered as a dependent proposition . I suppose in (classical) categorical semantics this is the indicator function of the subset of even primes . Then take to get the type of all even primes corresponding to the proposition “(n is prime) and (n is even)”, and which in semantics is indeed the set (in the trivial context=over the terminal object) . Then you can compare the two propositions in the empty context.
Maybe fire back the question: Do you think all true propositions are logically equal, no matter their mathematical content? “Every simply connected, closed 3-manifold is homeomorphic to the 3-sphere” and “1=1” are equal!?
This is really just propositions-as-types stuff, not yet getting to the full power of univalence.
I don’t think I would have anything different to say: those two points seem to me to cover it.
The first problem is that pernicious global equality relation that ZFC has inflicted on mathematicians’ collective consciousness. (-: We should only talk about two things being equal once we have fixed the type to which they belong. “The set of even primes” as a subset of cannot even be compared for equality with the proposition . But “the set of even primes” as an abstract set no longer remembers that its element is called “2” and therefore can certainly be equal to any other one-element set.
The second problem is, one might say, that mathematicians are used to comparing definitions of propositions for their sense, but definitions of other things (sets, numbers, functions, etc.) for their reference. We think of “” and “the number of isomorphism classes of normed division algebras over ” as the same number, where what is the same is their reference, not their sense. But we think of the Poincare conjecture and Fermat’s last theorem as different propositions, though what differs is only their sense; their reference is the same, namely the truth value “true”.
Thanks.
So is there then a further step of forgetting not only sense but also the origin in the h-level hierarchy?
singleton subset of a set abstract singleton set abstract (contractible) type
true proposition truth value “true” abstract (contractible) type
Noodling about, there’s a passage from to , and from to and it’s only then that and may be compared.
…different propositions, though what differs is only their sense; their reference is the same, namely the truth value “true”
Back to Frege (in that respect at least)!
Re: 37-38, yes I guess so, although that is more often treated as an implicit coercion. In particular, it is an embedding, so whether or not two sets or propositions are equal as sets or propositions is the same as whether they are equal as types.
Well I was thinking particularly about comparing across the apparent set/proposition divide.
Right, I know; I was just offering that as an explanation for why it’s relatively harmless to consider it an implicit coercion.
I hadn’t thought of it this way, but that idea that with subtypes of a given type, , identity is not just equivalence, can be seen as a case of propositional extensionality in the context of .
Does one ever speak of the univalence axiom in a context? Or is it that, since a slice is still an -topos, that there’s no need?
What I claim is demonstrably false is a mathematical statement like “we have to find a new way to formulate Galois theory”.
If one just works at the level of sets, and is not actually using univalence in any significant way, then of course one can proceed more or less as usual. What I was getting at is that if one tries to work more natively with general types (and the vast majority of interesting work in HoTT has been done in that setting), where univalence is more likely to play a more fundamental role, then, yes, this will be the case.
The point I was making is that any concrete example of such a replacement can also be done in classical mathematics
The distinction I was drawing is precisely that in classical mathematics one only can work at the level of this replacement. In univalent mathematics, one can make an abstract construction which does not unwrap the computation, and at that abstract level, i.e. without unwrapping to a computation, there is no difference at all in what one can do, whether one has an integer or something else which one is identifying it with under univalence.
It’s not nitpicking to point out that “squashing” is the identity map
It was important to what I was saying that the ’squashing’ is not to be viewed as a construction on/in . What I was saying is that one takes one of the arrows of the latter, forgets the fact that it is an arrow of it and just remembers that it is a homotopy class of loops in , and then squashes, obtaining some other homotopy class of loops in .
43 I hadn’t thought of it this way, but that idea that with subtypes of a given type, , identity is not just equivalence, can be seen as a case of propositional extensionality in the context of .
I thought in logical type theories (as apposed to some CS type systems) there is no notion of subtype - every term has a single type. Logically the integers are not a subtype of the reals.
For subtypes, see p. 115 of the HoTT book. I’m even using it in the “more correct” way for remembering its relation to the type.
If one just works at the level of sets, and is not actually using univalence in any significant way, then of course one can proceed more or less as usual.
This alone is enough to make the statement “we have to find a new way to formulate Galois theory” highly misleading, and something that should not be said in the hearing of newcomers who are confused about basic aspects of univalence.
I don’t see any reason to believe that anything different happens for higher types either – after all, one of the whole points of HoTT is that higher types are not qualitatively different from sets – but I’m tired of trying to guess what you mean, so if you want to continue this conversation please make a precise mathematical statement.
after all, one of the whole points of HoTT is that higher types are not qualitatively different from sets
I think this is nonsense, actually.
if you want to continue this conversation please make a precise mathematical statement.
I am not in the least interested in continuing the conversation, I entered it primarily because I felt that I might be able to defend a bit more strongly a point that I felt was underlying Jrich22’s questions. A secondary reason was because there tends to be a dismissive tone adopted in these kind of discussions from the knowing in the club to the presumed unknowing newcomer (i.e. Jrich22), which I felt it healthy to counter. I knew full well that my comments would be treated with dismissal, but I felt it important for someone to raise their head above the parapet. I have long had enough, however, of the tone of the discussion, as I have had in earlier discussions of this nature, and I leave it to those in the club to wink to one another further, should they wish. Whether or not the points I have been making have been understood, I stand by them.
I generally try very hard not to be dismissive to the unknowing newcomer who admits their ignorance. But as I said, I feel it necessary to take a strong line when someone presents a misinformed position with an authoritative tone, since otherwise that could further confuse the other unknowing newcomers.
(Obviously there are some qualitative differences between higher types and sets, but not as regards something fundamental like whether we can talk about their automorphisms.)
Just in case it helps for the future, let me point out that whilst it may simply be careless, use of language like ’misinformed’ is very unfortunate. What right do you or I or anybody else have to decide whether somebody is ’informed’, when it is mathematics we are talking about? Mathematics is not about being ’informed’ or ’misinformed’, this is a sociological construct, and the very thing I was railing against.
Replying to myself (#43), see A.3.1, univalence defined in a context.
Mathematical facts are not a sociological construct. Is “mistaken” or “incorrect” better than “misinformed”?
1 to 52 of 52