Is there a flat-modality in A1-homotopy theory?

[felixwellen]

This (hopefully) boils down to the following external question:
Let $i:M\to\mathrm{Sh}(\mathrm{Zar})$ be the inclusion of the $\mathbb A^1$-local sheaves into all Zariski-sheaves. Then the localization is a left adjoint to $i$ and the question if there is a flat modality should be the question if $i$ also has a right adjoint or equivalently preserves homotopy colimits. I am not sure if that would be enough, but if it is false, we can definitely start to seriously question #17 .
Assuming a flat-modality, it should work to use David Jaz Myers idea in the good fibrations article, theorem 5.9 taking for X the type of torsors of crisply discrete groups, to show #17.

[felixwellen]

From a discussion with David this morning: No, there cannot be a flat-modality like that, because the coalgebras of a lex comonad on a topos is a topos. A flat modality should be lex, because it is crisply right-adjoint to A1-nullfication. So this should show that externally, a flat modality would imply that the A1-local objects form a topos, which is known to be false.

[felixwellen]

Written down in README

[xuanruiqi]

I think we can maybe reopen this issue. Recently I've been looking deeper into cohesive HoTT, and while I still claim to be no expert of it, it does look to me that some form of ($\mathbb{A}^1$-cohesive) HoTT is definitely the right setting for synthetic motivic homotopy theory.

Perhaps this boils down to the choice of site (the Nisnevich vs. étale stuff we'd discussed briefly at SAG 4) - so maybe we just don't have the right shape modality yet? Anyways this has been in my head for quite a few days, so just some simple thoughts for the moment.

Of course, if we're going into the stable theory, that's a wholly different beast - but I guess no one's thinking that far yet...

[xuanruiqi]

Never mind, I opened a new issue to discuss this line of thought.