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
-
-
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.
1 reply 0 retweets 2 likes -
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
I appreciate your trying, though!
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.