Modalities and Parametric Adjoints

• Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.

Ämnesord

NATURVETENSKAP  -- Matematik (hsv//swe)

NATURAL SCIENCES  -- Mathematics (hsv//eng)

Nyckelord

Modal types

dependent types

Fitch-style modalities

categorical semantics

parametricity

guarded recursion

Publikations- och innehållstyp

ref (ämneskategori)

art (ämneskategori)