Mathetmatics

  • The !-modality Is a Comonad

    by Vanessa McHale | Mathetmatics

    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 \).