5
$\begingroup$

Presheaf toposes satisfy LPO and (edit: if over categories with binary products) PAx and countable choice internally, so they automatically satisfy the stable fan theorem (every bar which is the intersection of a countable family of decidable bars is uniform), which is a fairly strong version of the fan theorem.

Do presheaf toposes satisfy the full fan theorem (all bars are uniform) internally? And while we are at it, do they satisfy open induction and maybe also the decidable bar theorem?

Improve this question
$\endgroup$
4
  • $\begingroup$ Can you provide evidence for the claim that presheaf toposes satisfy countable choice and LPO? $\endgroup$
    – Andrej Bauer
    Commented Jul 7, 2023 at 12:40
  • 1
    $\begingroup$ @AndrejBauer They satisfy countable choice because they have enough projectives, which implies COSHEP, so they satisfy CC and DC. Looking at nlab, they satisfy arithmetic LPO because presheaf toposes are locally connected, and for locally connected grothendieck topoi 2^N is a constant sheaf. CC + arithmetic LPO implies the analytic LPO so we do not need to make the distinction. It does look like the observation about 2^N being a constant sheaf is the key observation to make here to prove the full fan theorem here though $\endgroup$
    – saolof
    Commented Jul 7, 2023 at 12:47
  • $\begingroup$ (Also, as a sidenote, Fourman & Hylland state in theorem 3.7 of Sheaf models for analysis, that for spatial topoi being locally connected implies the decidable bar theorem, and make an informal argument that the proof works for locales and works constructively assuming only that the decidable bar theorem holds externally) $\endgroup$
    – saolof
    Commented Jul 7, 2023 at 12:51
  • 1
    $\begingroup$ Thank you. (This text is here because comments must be at least 15 characters in length.) $\endgroup$
    – Andrej Bauer
    Commented Jul 7, 2023 at 15:53

0

Reset to default

You must log in to answer this question.