Timeline for Constructively, is the unit of the “free abelian group” monad on sets injective?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 3, 2022 at 0:53 | comment | added | Todd Trimble | @PeterLeFanuLumsdaine Oh, I see. Very nice! And simple indeed. Thank you! | |
| Oct 2, 2022 at 9:51 | comment | added | Peter LeFanu Lumsdaine | @ToddTrimble: 4 years later, I have an answer to your question “Is there a general class of algebraic theories […] where the unit of the monad is injective, constructively?” — yes, this holds for any finitary algebraic theory that has some model with two distinct elements! See my comments on David Wärn’s new answer. With such a straightforward proof, it seems bizarre that we all missed this in 2018… | |
| Feb 22, 2022 at 10:45 | vote | accept | Peter LeFanu Lumsdaine | ||
| Oct 2, 2022 at 9:45 | |||||
| Jun 12, 2018 at 8:22 | comment | added | Peter LeFanu Lumsdaine | @WillSawin: Regardless of the trees/lists difference, the construction of the free algebra as “syntax” certainly works fine constructively. However, the elements of the set $X$ still end up appearing in that syntax (depending on presentation, either as the variables or as the constant symbols, in any case as the leaves of the syntax tree), so this “syntax” may fail to have decidable equality; and so it’s still not clear to me how to carry through an argument that it holds constructively iff it holds in usual mathematics. | |
| Jun 12, 2018 at 7:30 | comment | added | Andrej Bauer | @WillSawin: yes, it is "just a notational difference" in the same way that abstract linear algebra is "the same as matrices". It's a matter of working at the correct level of abstraction. Working with trees encoded as strings is as cumbersome and annoying as working with mathematical structures needlessly encoded as sets. | |
| Jun 12, 2018 at 5:29 | comment | added | David Roberts♦ | In your opening paragraph, do you mean $\to$ instead of $\mapsto$? | |
| Jun 11, 2018 at 22:29 | comment | added | Will Sawin | @AndrejBauer Isn't this just a notational difference, because we can transform ordered trees into ordered lists and vice versa? I agree the tree notation is nicer. | |
| Jun 11, 2018 at 20:29 | comment | added | Andrej Bauer | @WillSawin: trees, use trees instead of lists. Peter is using lists because he can juggle associativity on his nose. | |
| Jun 11, 2018 at 19:55 | comment | added | Will Sawin | @ToddTrimble If an algebraic theory is generated by some function symbols and some relations, I would think we can express elements of the free object as lists of the union of the set of function symbols and elements of the base set (say in reverse Polish notation), satisfying some rules, up to an equivalence relation of chains of valid algebraic manipulations using the relations. Expressed this way, I would think that it holds constructively if and only if it holds in the usual mathematics, because the only way to make two things equivalent is by an explicit construction. | |
| Jun 11, 2018 at 12:14 | comment | added | Todd Trimble | Thanks very much for writing out the details, Peter. Is there a general class of algebraic theories one can name where the unit of the monad is injective, constructively? | |
| Jun 11, 2018 at 9:49 | comment | added | Harry Gindi | @Andrej It means precisely that! | |
| Jun 11, 2018 at 9:14 | comment | added | Andrej Bauer | Very nice! By the way, outside category theory people might wonder if "holding on the nose" has anything to do with sea lions' juggling abilities. | |
| Jun 11, 2018 at 8:23 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |