nLab modalities - contents

modal type theory, modal logic

closure operator, universal closure operator

• idempotent monad, comonad

• modal type, local object

• reflective subcategory, coreflective subcategory

Examples

• Moore closure

• geometric modality/Lawvere-Tierney topology

• S4 modal logic

• n-truncation

• shape modality$\dashv$ flat modality $\dashv$ sharp modality