Same. No there there
-
-
Replying to @Meaningness
The treatments I've seen just talk in circles around the subject without getting down to anything concrete. And no results! Just handwaving.
1 reply 0 retweets 3 likes -
Replying to @St_Rev @Meaningness
"we replace homotopy, which is a fairly delicate mathematical construction whose existence has to be checked and proven, with...a colon, which just sits there and magically does the same thing"
1 reply 0 retweets 3 likes -
Replying to @St_Rev
In practice the point seems to be that it provides a notation for expressing simple properties of programs like "returns a vector of positive integers."
2 replies 0 retweets 2 likes -
Replying to @Meaningness @St_Rev
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...2 replies 0 retweets 1 like -
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 -
Replying to @11kilobytes @Meaningness and
What really requires this stuff to be non-trivial is the univalence axiom ("equality is canonically equivalent to equivalence") that requires everything to be homotopy invariant in a way compatible with term-reduction.
1 reply 0 retweets 0 likes
Term reduction is also a discrete process? What is the topology on terms?
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.