${\text{TT}}_{\mathcal{C}}^{\square }$: a Family of Extensional Type Theories with Effectful Realizers of Continuity

Liron Cohen, Vincent Rahli

${\text{TT}}_{\mathcal{C}}^{\square }$ is a generic family of effectful, extensional type theories with a forcing interpretation parameterized by modalities. This paper identifies a subcl…