On a local topos/local (∞,1)-topos $\mathbf{H}$, hence equipped with a fully faithful extra right adjoint $coDisc$ to the global section geometric morphism $(Disc \dashv \Gamma)$, is induced an idempotent monad $\sharp \coloneqq coDisc \circ \Gamma$, a modality which we call the sharp modality. This is itself the right adjoint in an adjoint modality with the flat modality $\flat \coloneqq Disc \circ \Gamma$.
The codiscrete objects in a local topos are the modal types for the sharp modality.
The discrete objects in a local topos are the modal types for the flat modality.
(shape modality $\dashv$ flat modality $\dashv$ sharp modality)
$(ʃ \dashv \flat \dashv \sharp )$
(reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)
$(Red \dashv ʃ_{inf} \dashv \flat_{inf})$
See the references at local topos.