These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.