Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorJrich22
    • CommentTimeNov 9th 2017
    Bourbaki structuralism can be characterized, roughly, as treating isomorphic objects as indistinguishable and so identical by Leibniz's law. In practice, we don't have to distinguish between isomorphism and (numerical) identity (or should not have to).

    I was recently Barr's translation of Grothendieck's Tohoku paper and he said something (in his preface) that, which now seems obvious, I had not thought of: how can one make sense of Galois theory, which depends on the notion of automorphism group, without being able to distinguish between isomorphism and identity?

    How does HoTT and univalence deal with this?

    I apologize if this question has already been discussed in detail.
    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 10th 2017

    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.

    • CommentRowNumber3.
    • CommentAuthorJrich22
    • CommentTime6 days ago
    Thank you.

    I understand the conceptual move of seeing univalence as a generalization instead of a collapse, and I'll take your point that all the isomorphisms and so automorphisms are still there, but how does one distinguish an automorphism from an isomorphism that is not one? If you could point to a text in which this type of stuff is worked out in HoTT, that would be great!

    Is your point related to the fact that if any isomorphisms from some object A to B exist, then there are the same number of them as automorphisms of A?
    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTime6 days ago

    The type of isomorphisms from AA to BB is ABA\cong B. The type of automorphisms of AA is AAA\cong A. So an automorphism is the special case of an isomorphism where the two objects are the same.

    • CommentRowNumber5.
    • CommentAuthorJrich22
    • CommentTime6 days ago
    For sure. That's just the standard definition. My question concerns how it even makes sense given univalence. Univalence seems to say that automorphisms are the same things as isomorphisms, so the former type cannot be special cases of the latter type.

    I don't see how the conceptual move of viewing univalence as a generalization and not a collapse gets around this, i.e., how it permits us to distinguish automorphisms from isomorphisms that are not automorphisms.

    For instance, you write: an automorphism is a special case of isomorphism where two objects are the same. What do you mean by 'the same' here? If you just mean isomorphic, then we have: automorphisms are isomorphisms where the two objects involved are isomorphic. This doesn't distinguish automorphisms from isomorphisms that are not automorphisms. It seems to say there is no difference.

    I'm sincerely not trying to be difficult here. There just seems to be some fundamental point I'm failing to get here.
    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTime6 days ago
    • (edited 6 days ago)

    Univalence says that the type A=BA=B of identities/equalities/identifications between two types AA and BB is equivalent to the type ABA\cong B of isomorphisms/equivalences between them. This is also true when AA and BB are the same, so that A=AA=A is equivalent to AAA\cong A. If AA and BB are equivalent, then ABA\cong B is also equivalent to AAA\cong A by composing with that equivalence, and likewise A=BA=B is equivalent to A=AA=A by composing with the corresponding identification. The equivalence (A=B)(A=A)(A=B)\cong (A=A) then itself passes across univalence to become an identification (A=B)=(A=A)(A=B) = (A=A). But that doesn’t mean that any element of A=BA=B is itself an element of A=AA=A; you have to explicitly transport it across that identification.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTime6 days ago
    • (edited 6 days ago)

    Since this kind of issue is good practice for me, explaining to colleagues, let me butt in. AA is canonically isomorphic to AA along id Aid_A.

    You have a canonical isomorphism in Equiv(A,A)Equiv(A, A) for all types AA, using the id construction on p. 26 of the HoTT book. This will correspond to the ’refl’ elements in Id 𝒰(A,A)Id_{\mathcal{U}}(A, A). For AA and BB equivalent (isomorphic) there is no canonical such equivalence.

  1. Mike,

    This is also true when AA and BB are the same, so that A=AA=A is equivalent to ABA\cong B.

    Was the final symbol supposed to be AA? I

    I guess the question is asking what you mean by “same” there.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTime6 days ago

    Was the final symbol supposed to be AA?

    Yes, fixed, thanks.

  2. I would say that Jrich22’s point is essentially valid. Take for example a connected groupoid GG. For an object xx of GG, we can consider Aut(x)Aut(x), namely Hom(x,x)Hom(x,x). Now, GG is equivalent to a groupoid AA with a single object. In AA, we have lost the ability to speak about Aut(x)Aut(x), there is no way to recover it from AA alone. And if the philosophy is that we should be carrying out constructions which can be carried out equally well in GG or AA, 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 GG to AA.

    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.

  3. Sorry, what have we lost? AA has a single object, say *\ast. Then in the type theory, Id A(*,*)Id G(x,x)Id_A (\ast, \ast) \simeq Id_G (x, x). Or if you prefer to talk from the point of view of category theory, Hom G(x,x)Hom A(*,*)Hom_G(x, x) \cong Hom_A(\ast, \ast).

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTime5 days ago

    Rubbish. Any equivalence f:GAf:G\simeq A induces an isomorphism from Aut(x)Aut(f(x))Aut(x) \cong Aut(f(x)). Of course different equivalences ff 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 G=AG=A to remember which equivalence we’re talking about.

    • CommentRowNumber13.
    • CommentAuthorUlrik
    • CommentTime5 days ago

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

    • CommentRowNumber14.
    • CommentAuthorRichard Williamson
    • CommentTime5 days ago
    • (edited 5 days ago)

    In reply to #11 and #12: one can speak about the groupoid of automorphisms of Aut(x)Aut(x), but not Aut(x)Aut(x) itself, i.e. we can know Aut(x)Aut(x) up to isomorphism, but not up to equality, and knowing it up to isomorphism in fact encompasses all isomorphisms in GG, not only automorphisms of xx. 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.)

  4. Regarding #13: yes, certainly, the fact that we have to choose an object of GG 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.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTime5 days ago

    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 Aut(x)Aut(x) (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 GG. There is no need for any change in how we formulate Galois theory: if GG is a groupoid and xGx\in G then Aut(x)Aut(x) 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 GG yields an equivalence to a one-object groupoid doesn’t change this.

    • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTime5 days ago
    • (edited 5 days ago)

    The choice of an object xx in GG together a term of type y:Obj(G)G(x,y)\prod_{y:Obj(G)} G(x, y) , no?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTime5 days ago

    @DavidRoberts: Well, it depends on what exactly you want to determine and how. Choosing an object xGx\in G determines a one-object groupoid BAut(x)B Aut(x) and a functor BAut(x)GB Aut(x) \to G that’s fully faithful and essentially surjective, and its inverse equivalence is then determined up to a contractible space of choices.

    • CommentRowNumber19.
    • CommentAuthorDavidRoberts
    • CommentTime5 days ago

    Sure, good point.

    • CommentRowNumber20.
    • CommentAuthorRichard Williamson
    • CommentTime5 days ago
    • (edited 5 days ago)

    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 GG to replace Aut(x)Aut(x) by an object isomorphic to it, and depending on which choice of Aut(x)Aut(x) in its isomorphism class one is looking at, amongst those arising in this way, the elements are not necessarily automorphisms of xx in the original sense, they are conjugated with the chosen isomorphism. One has lost the ability to refer to automorphisms of xx 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.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTime5 days ago
    • (edited 5 days ago)

    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.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

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

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    Urs, you’re absolutely right; someone just has to find the time…

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

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    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.

    • CommentRowNumber26.
    • CommentAuthorRichard Williamson
    • CommentTime4 days ago
    • (edited 4 days ago)

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

    • CommentRowNumber27.
    • CommentAuthorRichard Williamson
    • CommentTime4 days ago
    • (edited 4 days ago)

    Found a little time. Maybe the following will help. In univalence, given any construction which we can make with Aut(x)Aut(x) and f:Aut(x)f : Aut(x), we can replace Aut(x)Aut(x) by Aut(y)Aut(y) if xx and yy are isomorphic, and replace ff by something in Aut(y)Aut(y) (its conjugate). This is the elimination rule for identity types. So, for all purposes, ff is as good as its counterpart in Aut(y)Aut(y).

    But ff 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 Π 1(S 1)\Pi_{1}(S^{1}) \simeq \mathbb{Z}, viewing the latter as a one-object groupoid. I might take some point on S 1S^{1}, take some loop at that point, and squash it in 2\mathbb{R}^{2} so that it becomes an oval. This is meaningless for the zz \in \mathbb{Z} 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.

  6. Aren’t you mixing up circle in the two senses?

    1. The higher inductive type with constructors base:Circlebase: Circle, and loop:Id Circle(base,base)loop: Id_{Circle}(base, base).
    2. The sub-0-type of 2\mathbb{R}^2 which given some construction of the latter as a 0-type picks out a circle.

    There’s no problem surely in the former case of identify the fundamental group with \mathbb{Z}. 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 2\mathbb{R}^2. This cannot be taken as equivalent to the 1-type, BB \mathbb{Z}, 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 ʃS 1 ʃ S^1, where S 1S^1 is your second kind of circle. This is here the fundamental groupoid, yielding a 1-type equivalent to BB \mathbb{Z}. Of course, ʃ loses all but homotopical information.

    • CommentRowNumber29.
    • CommentAuthorRichard Williamson
    • CommentTime4 days ago
    • (edited 4 days ago)

    I was thinking of S 1S^{1} as a topological space embedded in 2\mathbb{R}^{2}, however we define that in HoTT, and Π 1(S 1)\Pi_{1}(S^{1}) as the groupoid whose objects are points of S 1S^{1}, and whose arrows are paths between them up to homotopy; again, however we define that in HoTT. The arrows are paths embedded in 2\mathbb{R}^{2}. One should be able, one day at least, to prove in HoTT that Π 1(S 1)\Pi_{1}(S^{1}) in this sense is equivalent to BB\mathbb{Z} (the proof may use the other definition of S 1S^{1}, or it may not). The two types Π 1(S 1)\Pi_{1}(S^{1}) and BB\mathbb{Z} are at the same level; it doesn’t matter what level S 1S^{1} itself is at, as you essentially point out at the end of your comments.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTime3 days ago

    In univalence, given any construction which we can make with Aut(x)Aut(x) and f:Aut(x)f : Aut(x), we can replace Aut(x)Aut(x) by Aut(y)Aut(y) if xx and yy are isomorphic, and replace ff by something in Aut(y)Aut(y) (its conjugate). This is the elimination rule for identity types. So, for all purposes, ff is as good as its counterpart in Aut(y)Aut(y).

    This is equally true in classical mathematics: you can always conjugate ff by an isomorphism xyx\cong y to obtain an automorphism of yy. There is nothing different about univalence here.

    I might take some point on S 1S^{1}, take some loop at that point, and squash it in 2\mathbb{R}^{2} so that it becomes an oval.

    That is not in any foundations a meaningful (nontrivial) construction on automorphisms of a point in Π(S 1)\Pi(S^1), which are homotopy classes of paths in S 1S^1.

    • CommentRowNumber31.
    • CommentAuthorRichard Williamson
    • CommentTime3 days ago
    • (edited 3 days ago)

    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 Aut(x)Aut(x) and f:Aut(x)f : Aut(x) by Aut(y)Aut(y) and the conjugation of ff. 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 Π 1(S 1)\Pi_{1}(S^{1}), rotate, then go back to \mathbb{Z}, 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.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTime3 days ago

    I think you missed the actual point I was making, that in univalent mathematics we can formally replace in any construction Aut(x)Aut(x) and f:Aut(x)f : Aut(x) by Aut(y)Aut(y) and the conjugation of ff. 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 Π 1(S 1)\Pi_1(S^1); the point is that it’s something that does make sense for \mathbb{Z} as well, since \mathbb{Z} also has an identity map. Univalence does give you a way to transfer an integer to a loop in S 1S^1, 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.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTime3 days ago

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

  7. 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 𝒰\mathcal{U} doesn’t mean there is the conceptual relation of definitional equality.

    Is there more to say?

    • CommentRowNumber35.
    • CommentAuthorDavidRoberts
    • CommentTime3 days ago

    The set of all even primes can be considered via the proposition ϕ(n)=\phi(n)= “(n is prime) and (n is even)”, considered as a dependent proposition n:ϕ(n):Propn\colon \mathbb{N} \vdash \phi(n):Prop. I suppose in (classical) categorical semantics this is the indicator function {0,1}\mathbb{N} \to \{0,1\} of the subset of even primes {2}\{2\} \hookrightarrow \mathbb{N}. Then take Σ n:\Sigma_{n\colon \mathbb{N}} to get the type of all even primes corresponding to the proposition n:\exists n\colon \mathbb{N}“(n is prime) and (n is even)”, and which in semantics is indeed the set (in the trivial context=over the terminal object) {2}\{2\}. 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.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTime3 days ago

    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 \mathbb{N} cannot even be compared for equality with the proposition 2+2=42+2=4. 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 “2+22+2” and “the number of isomorphism classes of normed division algebras over \mathbb{R}” 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”.

  8. 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 \to abstract singleton set \to abstract (contractible) type

    • true proposition \to truth value “true” \to abstract (contractible) type

  9. Noodling about, there’s a passage from (X,s):Set 𝒰(X, s): Set_{\mathcal{U}} to X:𝒰X: \mathcal{U}, and from (Y,t):Prop 𝒰(Y,t):Prop_{\mathcal{U}} to Y:𝒰Y: \mathcal{U} and it’s only then that XX and YY may be compared.

  10. …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)!

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTime3 days ago

    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.

  11. Well I was thinking particularly about comparing across the apparent set/proposition divide.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTime2 days ago

    Right, I know; I was just offering that as an explanation for why it’s relatively harmless to consider it an implicit coercion.

    • CommentRowNumber43.
    • CommentAuthorDavid_Corfield
    • CommentTime1 day ago
    • (edited 1 day ago)

    I hadn’t thought of it this way, but that idea that with subtypes of a given type, AA, identity is not just equivalence, can be seen as a case of propositional extensionality in the context of AA.

    Does one ever speak of the univalence axiom in a context? Or is it that, since a slice is still an (,1)(\infty, 1)-topos, that there’s no need?

    • CommentRowNumber44.
    • CommentAuthorRichard Williamson
    • CommentTime1 day ago
    • (edited 1 day ago)

    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 Π 1(S 1)\Pi_{1}(S^{1}). 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 2\mathbb{R}^{2}, and then squashes, obtaining some other homotopy class of loops in 2\mathbb{R}^{2}.

    • CommentRowNumber45.
    • CommentAuthorRodMcGuire
    • CommentTime1 day ago

    43 I hadn’t thought of it this way, but that idea that with subtypes of a given type, AA, identity is not just equivalence, can be seen as a case of propositional extensionality in the context of AA.

    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.

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

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTime48 minutes ago

    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.