Modalities and Parametric Adjoints

DOI10.1145/3514241MaRDI QIDQ5072609zbMATH OpenOpenAlexFDO

Authors Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal

Publication date 29 April 2022

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3514241

zbMATH Keywords

categorical semanticsdependent typesFitch-style modalitiesguarded recursionmodal typesparametricity

Mathematics Subject Classification ID

Type theory (03B38) Modal logic (including the logic of norms) (03B45) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Recommendations

• Modes of adjointness
• On monotone modalities and adjointness
• scientific article; zbMATH DE number 67510
• Adjoining adjoints
• scientific article; zbMATH DE number 2165869
• Adjoints, multi-adjoints, pluri-adjoints
• Adjoint action and its generalizations
• Modality, quantification, and many Vlach-operators
• Adjoint multidimensional acausal systems
• scientific article; zbMATH DE number 1286232

Cited in

(16)

• Fibrational modal type theory
• scientific article; zbMATH DE number 67510 (Why is no real title available?)
• Multimodal dependent type theory
• Multimodal dependent type theory
• Modal dependent type theory and dependent right adjoints
• Origins of parameters in adimensional models
• When programs have to watch paint dry
• Strange new universes: Proof assistants and synthetic foundations
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Transpension: the right adjoint to the Pi-type
• Normalization for multimodal type theory
• Two-dimensional Kripke semantics. II: Stability and completeness
• Semantics of multimodal adjoint type theory
• Normalization for multimodal type theory
• Two-dimensional Kripke semantics i: presheaves
• Displayed type theory and semi-simplicial types

This page was built for publication: Modalities and Parametric Adjoints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5072609)