https://arxiv.org/abs/1708.02143 Litak, Visser, "Lewis meets Brouwer: constructive strict implication"

Известно, что монадические и комонадические исчисления соответствуют по Карри-Говарду модальным логикам с унарной модальностью □, а как насчёт стрелок Хьюза? Оказывается, им соответствует двухместная модальность ⥽, так называемая "строгая импликация". Более того, изначальная формулировка модальной логики по Льюису вводила именно строгую импликацию как первичный конструкт, а □ выражалась через неё. После ряда работ Гёделя стрелку забыли в пользу коробки, в том числе потому, что в классическом варианте эти модальности взаимовыразимы. Как водится, в конструктивной формулировке симметрия распадается на независимые сущности, имеющие разные семантики - добавляя к строгим импликациям дополнительные схемы, можно получить логику для стрелок или любимой тотальщиками guarded recursion (кстати, как по русски - охраняемая рекурсия?).