Timeline for Injectivity implies left inverse in Bishop's constructive mathematics
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5 at 11:50 | vote | accept | Pavlo Surzhenko | ||
| Nov 5 at 11:46 | comment | added | Naïm Camille Favier | Yes. I am working in type theory where propositions are types all of whose elements are equal, but you may translate this into set theory by taking the set $\{\ast \mid P\}$. | |
| Nov 5 at 11:45 | comment | added | Pavlo Surzhenko | Do I understand correctly, here $P$ is thought of as the set of proofs of $P$, where all the proofs are considered equal, and $1$ is the set $\{*\}$? | |
| Nov 5 at 11:34 | history | answered | Naïm Camille Favier | CC BY-SA 4.0 |