Timeline for Constructively, is the unit of the “free abelian group” monad on sets injective?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 14, 2018 at 12:08 | comment | added | Peter LeFanu Lumsdaine | @IngoBlechschmidt: I agree this is another nice alternative description of the equivalence relation, but I don’t think your or my characterisations require cancellativity? At least mine doesn’t, unless I have made an error somewhere (I state it for rigs from the start!), and the indirect argument I had for yours doesn’t either (showing that your relation implies mine, by inductively building up a colouring by repeatedly using your criterion on any remaining “uncoloured” elements)? | |
| Jun 12, 2018 at 12:28 | history | edited | Itai Bar-Natan | CC BY-SA 4.0 |
added 7 characters in body
|
| Jun 12, 2018 at 12:20 | comment | added | Ingo Blechschmidt | Very nice! Unlike mine and like Peter's, your proof doesn't require cancellability, so generalizes to modules over rigs. In fact, I believe that your proof can be homotoped to Peter's proof. | |
| Jun 12, 2018 at 11:58 | history | answered | Itai Bar-Natan | CC BY-SA 4.0 |