Author: spitters Format: MarkdownItexStrengthening the statement of the work by Mike on the interpretation of HoTT in higher toposes.
<a href="https://ncatlab.org/nlab/revision/diff/Johnstone%27s+topological+topos/23">diff</a>, <a href="https://ncatlab.org/nlab/revision/Johnstone%27s+topological+topos/23">v23</a>, <a href="https://ncatlab.org/nlab/show/Johnstone%27s+topological+topos">current</a>
Strengthening the statement of the work by Mike on the interpretation of HoTT in higher toposes.
Author: nLab edit announcer Format: MarkdownItexJohnstone's topological topos satisifies dependent choice; reference added to a pdf with a proof by Shulman and Simpson.
Tom de Jong
<a href="https://ncatlab.org/nlab/revision/diff/Johnstone%27s+topological+topos/25">diff</a>, <a href="https://ncatlab.org/nlab/revision/Johnstone%27s+topological+topos/25">v25</a>, <a href="https://ncatlab.org/nlab/show/Johnstone%27s+topological+topos">current</a>
Johnstone’s topological topos satisifies dependent choice; reference added to a pdf with a proof by Shulman and Simpson.