modal type theory, modal logic
closure operator, universal closure operator
idempotent monad, comonad
modal type, local object
reflective subcategory, coreflective subcategory
geometric modality/Lawvere-Tierney topology
S4 modal logic
Pi modality ⊣ flat modality ⊣ sharp modality
On a local topos H acts a comonad ♭, being the left adjoint to the monad ♯ induces by the extra right adjoint of the global section geometric morphism. This is the flat modality on the topos.
The codiscrete objects in a local topos are the modal types for the sharp modality.
The discrete object in a local topos are the modal types for the flat modality.
(shape modality ⊣ flat modality ⊣ sharp modality)
discrete object, codiscrete object, concrete object
structures in cohesion
(reduction modality ⊣ infinitesimal shape modality ⊣ infinitesimal flat modality)
(Red⊣ʃ inf⊣♭ inf)
reduced object, coreduced object, formally smooth object
formally étale map
structures in differential cohesion
See the references at local topos.