Timeline for Are paths in HoTT perhaps just "cost-free" paths?
Current License: CC BY-SA 3.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 9, 2013 at 22:11 | comment | added | Mike Shulman | @DavidSpivak, are your maps $f$ required to preserve endpoints? And then, you have a category, and what is the functor defined on that category of which you are taking the colimit? | |
| Nov 8, 2013 at 17:29 | comment | added | Noam Zeilberger | @DavidSpivak Okay. As I wrote in my answer, I think the basic idea of "mutations as paths with costs" makes sense, and corresponds well with the basic judgments of Hoare logic (where the "cost" of a mutation is the command by which it is realized). However, in that interpretation, cost-free path = vertical morphism, and so I don't quite see where you are going in defining the space $X_0$. Would you still apply this construction if weights were generalized to be maps of an arbitrary category, rather than elements of a monoid? | |
| Nov 8, 2013 at 15:31 | comment | added | David Spivak | @Mike, the category has objects $P:[0,1]\to X$ and $Hom(P,Q)=\{f:[0,1]\to[0,1]\;|\;Q\circ f=P\}$. | |
| Nov 8, 2013 at 15:31 | comment | added | David Spivak | @Noam, in HoTT we have an identity type $Id_{x,y}$ for any two points $x,y\in X$, and I'm taking it to be the space of paths from $x$ to $y$ in $X_0$. | |
| Nov 6, 2013 at 23:50 | comment | added | Noam Zeilberger | @DavidSpivak can you explain what you meant by "identities" in Q1? | |
| Nov 6, 2013 at 14:48 | comment | added | Mike Shulman | It sounds like maybe what you want is the final topology (ncatlab.org/nlab/show/final+lift) on $X$ induced by all of the paths in question? I don't know offhand how to express that as a colimit. | |
| Nov 6, 2013 at 14:45 | comment | added | Mike Shulman | I'm just saying I don't know what the notation of your colimit means. Each $P$ is a map $[0,1]\to X$. How do you take the colimit of these? A colimit is a colimit of a functor; what is the functor and what is its domain? | |
| Nov 5, 2013 at 22:56 | comment | added | David Roberts♦ | Sounds like you want a mashup of HoTT and Finsler geometry | |
| Nov 5, 2013 at 15:38 | comment | added | David Spivak | Mike, I think CW complexes $X$ are "path generated" in the sense that, if we make all paths cost-free and let $X_0$ be my colimit, there is a homeomorphism $X_0\to X$. This space $X_0$ is constructed simply as a 1-categorical colimit in $Top$. In other words, I believe that to map out of a CW complex $X$, it suffices to make a coherent decision about where to send paths in $X$. Do you agree, and does this help explain "what my colimit is supposed to mean"? | |
| Nov 5, 2013 at 12:05 | comment | added | Urs Schreiber | My impression was that David is not after invertible paths, as in the fundamental groupoid, but wants non-invertible, directed paths that exhibit "genuine change". | |
| Nov 5, 2013 at 6:13 | comment | added | Mike Shulman | Your description of spaces whose paths have costs is interesting; probably you could encapsulate it as saying you have a space with a functor from its fundamental groupoid to the delooping of your monoid of costs. However, I don't understand what your colimit is supposed to mean, or in what way it results in a subset of $X$. Do you mean the classifying space of a certain topologized subgroupoid of the fundamental groupoid? | |
| Nov 4, 2013 at 22:09 | answer | added | Noam Zeilberger | timeline score: 4 | |
| Nov 4, 2013 at 20:07 | answer | added | Andrej Bauer | timeline score: 10 | |
| Nov 4, 2013 at 18:53 | answer | added | Urs Schreiber | timeline score: 4 | |
| Nov 4, 2013 at 18:40 | history | edited | David Spivak | CC BY-SA 3.0 |
edited title
|
| Nov 4, 2013 at 18:25 | comment | added | Jason Gross | Your question seems to assume that mutation is a sensical concept in dependent type theory, and I'm not convinced it is. Do you know of any sources that describe or define what "mutation" means in dependent type theory? Generally, purely functional languages deal with mutation by using monads, which hide the effects of mutation from the rest of the (purely functional) program. If I understand correctly, monads represent mutation by treating the rest of the program as a function which takes in the most recent value of the mutable variables, and then mutation is just function application. | |
| Nov 4, 2013 at 18:18 | comment | added | Qiaochu Yuan | My impression is that the style of programming closest to this kind of type theory is functional programming, which is in particular stateless, so you never change the value of anything. Also, the title of this question seems disconnected from the body. | |
| Nov 4, 2013 at 16:19 | comment | added | David Spivak | Thinking a bit more, it seems natural to let the monoid of costs, above ${\mathbb R}_+$, vary. A more versatile choice would be the cyclic monoid $M:=(\{0,\infty\},0,+)$, because a map $Path(X)\to M$ would not demand anything more than a description of "who is identical and who is not". | |
| Nov 4, 2013 at 16:16 | history | edited | David Spivak | CC BY-SA 3.0 |
added 174 characters in body
|
| Nov 4, 2013 at 15:28 | history | edited | David Spivak | CC BY-SA 3.0 |
deleted 136 characters in body
|
| Nov 4, 2013 at 15:01 | history | asked | David Spivak | CC BY-SA 3.0 |