Timeline for The groupoid of algebraic expressions and proofs
Current License: CC BY-SA 3.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 4, 2017 at 0:14 | comment | added | user40276 | This is the $\infty$-groupoid of computational paths (for your specific deductive system with reductions given accordingly). | |
| Mar 10, 2015 at 12:20 | comment | added | Sylvain JULIEN | ...that $A_{0}:=(\mathbb{Q},\mathbb{Q}(\sqrt{2}+\sqrt{3}))$ is a geodesics. | |
| Mar 10, 2015 at 12:14 | comment | added | Sylvain JULIEN | Sorry for answering that late. To me, the concept of geodesics as mentioned in my previous comment is the connection, if you consider passing from a differential field to an extension thereof as a path in the space of differential field extensions. You can ever consider the case of classical Galois theory, considering the two $3$-tuples $A:=(\mathbb{Q},\mathbb{Q}(\sqrt{2}),\mathbb{Q}(\sqrt{2},\sqrt{3})$ and $A'$ obtained from $A$ by the permutation $(23)$ as paths from $\mathbb{Q}$ to $\mathbb{Q}(\sqrt{2},\sqrt{3})$. The primitive element theorem then means.. | |
| Feb 23, 2015 at 5:42 | comment | added | goblin GONE | @SylvainJULIEN, that's an intense look question fella. What, in particular, do you think the connection might be? By the way, your previous comment made my day. :) | |
| Feb 23, 2015 at 5:14 | comment | added | Sylvain JULIEN | By the way, maybe your idea could shed a new light on a question of mine, namely mathoverflow.net/questions/154373/… | |
| Feb 20, 2015 at 16:13 | comment | added | Andrej Bauer | If you specify precisely how composition works (presumably an application of transitivity of equality) then there will be two ways of applyying transitivity for $a = b = c = d$, leading to the MacLane pentagon. Since you did not equate any proofs, you will not get associativity. | |
| Feb 20, 2015 at 10:57 | comment | added | goblin GONE | @AndrejBauer, well the path category of a quiver is associative precisely because the domain of the forgetful functor $\mathbf{Cat} \rightarrow \mathbf{Quiv}$ is $\mathbf{Cat}$. It should be the same thing here; by choosing an appropriate forgetful functor, with the correct domain, its left adjoint should build an associative structure "automatically". | |
| Feb 20, 2015 at 10:49 | comment | added | Andrej Bauer | How do you get composition to be associative? | |
| Feb 20, 2015 at 7:45 | comment | added | Sylvain JULIEN | It's too bad I can't upvote a dozen of times...I've been dreaming of such ideas for so long! But maybe a geometrical point of view of your groupoid would be useful too, especially if people like Maryam Mirzakhani or Misha Gromov got involved in expanding this sketch of theory. Maybe we could then use the concept of geodesics to formalize the pretty vague notion of "natural" or "direct" proof. Anyway, this question already made my day so thanks a lot for asking it! | |
| Feb 20, 2015 at 7:09 | answer | added | Giorgio Mossa | timeline score: 6 | |
| Feb 19, 2015 at 22:53 | answer | added | Anton Fetisov | timeline score: 4 | |
| Feb 15, 2015 at 9:00 | comment | added | goblin GONE | @PaulTaylor, now if you can see a way of describe the construction of interest by abstracting the concept "Lawvere theory" and considering "Lawvere theory objects in a $2$-category $\mathbf{C}$ with sufficient structure", and then choosing $\mathbf{C}$ carefully to explain the construction of interest, well this would be very interesting. I cannot currently see how to do this, however, and your answer offers absolutely no hints or suggestions in this direction. | |
| Feb 15, 2015 at 8:57 | comment | added | goblin GONE | @PaulTaylor, you misunderstand me. I would very much like to be able to view this as a special case of a more fundamental construction, perhaps the left-adjoint to some $2$-functor or some such. Nonetheless, the point remains that this groupoid-like-object is not a Lawvere theory in the usual sense of the word, and it cannot be recovered from the Lawvere theory. The act of passing from the presentation to the Lawvere theory throws away too much information, and we can't recover the groupoid of interest. | |
| Feb 14, 2015 at 18:28 | comment | added | Paul Taylor | Category Theory may seem complicated and arbitrary to outsiders, but in fact it has a tiny number of fundamental ideas and constructions, each of which is extremely versatile and powerful and may take one decades to appreciate fully. When you have found some construction, you will enhance your understanding by trying to identify how it is an instance or sometimes a variation on one of these fundamental constructions. If you try to make out that it is completely different then you will add to your own and others' confusion, not your understanding. | |
| Feb 13, 2015 at 18:52 | answer | added | Paul Taylor | timeline score: 3 | |
| Feb 13, 2015 at 16:58 | comment | added | François G. Dorais | @ZhenLin: The identity types lead to an $\infty$-groupoid structure. To get a plain groupoid, one needs to truncate... | |
| Feb 13, 2015 at 16:23 | comment | added | The Masked Avenger | There are those who might call a term algebra an absolutely free algebra. I call it a term algebra, the free countably generated algebra in the variety of all structures of a given similarity type. | |
| Feb 13, 2015 at 15:46 | comment | added | Zhen Lin | Look up higher inductive types in homotopy type theory. | |
| Feb 13, 2015 at 15:33 | answer | added | Joel David Hamkins | timeline score: 6 | |
| Feb 13, 2015 at 15:21 | comment | added | goblin GONE | @TheMaskedAvenger, do you mean absolutely free algebra? | |
| Feb 13, 2015 at 15:12 | comment | added | The Masked Avenger | Relatively free algebra with labelling of the term algebra by congruences. I don't recall seeing a categorification of the process as you have it here, but what you have above is not far removed from constructing the free algebra of a variety from a term algebra. | |
| Feb 13, 2015 at 15:04 | history | asked | goblin GONE | CC BY-SA 3.0 |