Timeline for Subcountability
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Apr 15 at 9:23 | history | suggested | C7X | CC BY-SA 4.0 |
Linkrot of original link
|
| Apr 15 at 7:24 | review | Suggested edits | |||
| S Apr 15 at 9:23 | |||||
| Dec 15, 2021 at 19:12 | vote | accept | ToucanIan | ||
| Dec 15, 2021 at 18:42 | comment | added | Ulrik Buchholtz | You picked about the most complicated case possible, because we need subset collection (or strong collection + fullness). In any case, looking at Rathjen's proof, you obtain the description by combining Aczel's sets-as-trees interpretation of CZF into a version of Martin-Löf type theory with one inductive type of trees, together with a recursive realizability interpretation. (The Cauchy reals also form a set and would be easier to represent directly via codes for recursive functions.) | |
| Dec 15, 2021 at 17:09 | comment | added | ToucanIan | How are real numbers, for example, represented as codes? I guess it’s necessary to specify the Dedekind reals since in CZF they form a set. | |
| Dec 14, 2021 at 18:28 | history | answered | Ulrik Buchholtz | CC BY-SA 4.0 |