Timeline for Constructively, is the unit of the “free abelian group” monad on sets injective?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 12, 2018 at 11:45 | comment | added | Ingo Blechschmidt | @Peter: I added a few details, and would like to apologize for the messy index-heavy proof. (In German we have a term for this: "Indexschlacht", literally "index battle".) Also thanks for reminding me of the proper notion, I changed "pseudo-ring" to "rig" to not contribute to unnecessary proliferation of terms. Darij: Yes, indeed, thank you; fixed. | |
| Jun 12, 2018 at 11:38 | history | edited | Ingo Blechschmidt | CC BY-SA 4.0 |
Added more details
|
| Jun 12, 2018 at 10:45 | history | edited | Ingo Blechschmidt | CC BY-SA 4.0 |
Fixed two typos
|
| Jun 11, 2018 at 19:46 | comment | added | darij grinberg | When you say $0 \in J'$, you mean $1 \in J'$? | |
| Jun 11, 2018 at 16:16 | comment | added | Peter LeFanu Lumsdaine | Very nice alternate characterisation! Could you expand on the argument you had in mind for your step 3? The only argument I am seeing for it right now is to show that your notion of similarity implies mine, but I guess this isn’t what you had in mind since (a) it would make your answer unnecessarily dependent on mine, and (b) (if I’m not mistaken) that argument then doesn’t require cancellativity but works fine also for pseudo-rings (i.e. what I called rigs in my answer). | |
| Jun 11, 2018 at 15:14 | history | answered | Ingo Blechschmidt | CC BY-SA 4.0 |