# blog

Mathetmatics
• ## The !-modality Is a Comonad

The !-modality is a comonad. In particular, it is a functor; we can lift any function/procedure to work on perennial types with map, $$A \multimap B \vdash !A \multimap !B$$.