From contexdt, I think @st_rev is talking specifically about homotopy type theory. I also don't know if there's a there there, but it's shiny. I seem to remember it at least motivated a new proof of a classic result, but I can't find it...
-
-
Replying to @postreptilian @St_Rev
Yeah I dunno, there’s so much excitement about it that once every few months I feel like I ought to figure out what it’s about, but every time I spend half an hour looking at it, it seems highly unpromising and I set it aside again.
1 reply 0 retweets 1 like -
E.g. it’s hard for me to imagine how homotopy, which is about continuous deformations of continuous functions, could give leverage in ToC, where nothing is continuous. Presumably I’m missing something because I haven’t even bothered to look this up, but
2 replies 0 retweets 0 likes -
To make an analogy: Euclid's Axioms :: Real Cartesian Plane as Homotopy Type Theory :: Spaces of various sorts. We work up to homotopy equivalence, so all the data you care about can be presented combinatorially...
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
e.g. the HoTT "circle" is freely generated by a point and a primitive-axiomatic path between that point and itself. This _means_, e.g. that to map it somewhere else is to give a loop there.
2 replies 0 retweets 0 likes -
I’m sorry, without reading up on a bunch of definitions, I don’t know what that means. How does homotopy apply to computation, in which all the “spaces” are at-most-countable sets of discrete objects? What is the topology?
1 reply 0 retweets 1 like -
Here's an analogy that might help: HoTT is to topology as Euclid's axioms are to the real coordinate plane. In Euclid's axioms we talk about points, by saying what you can do with them (construct lines, circles, intersections, etc.) instead of talking about the reals at all.
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
Similarly in HoTT we have a primitive Paths-Between(x, y) type for any x, y in a type A. It is primarily defined by the axiom that if you want to define something for arbitrary paths with unconstrained endpoints, you can assume that you are dealing with a constant path.
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
This axiomatises the "squishiness" of topology.
1 reply 0 retweets 0 likes -
Replying to @11kilobytes @Meaningness and
Now there is a certain subdiscipline of topology called algebraic topology, which is all about "counting," topological features of a space such as its number of holes. HoTT is really interested in the features of topological spacs that are visible to algebraic topology.
1 reply 0 retweets 1 like
Yes I get this in a vague way. I don’t think I’m going to get more without actually learning it, and I’m not motivated to do that because (so far) I haven’t seen that it is useful.
-
-
Replying to @Meaningness @11kilobytes and
Also, everything I’ve seen seems like it could be done much more simply in the framework of undergraduate abstract algebra.
1 reply 0 retweets 1 like -
Replying to @Meaningness @11kilobytes and
I appreciate your trying, though!
0 replies 0 retweets 1 like
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.