Constructing unprejudiced extensional type theories with choices via modalities

DOI10.4230/LIPICS.FSCD.2022.10MaRDI QIDQ6544102zbMATH OpenFDO

Authors Liron Cohen, Vincent Rahli

Publication date 27 May 2024

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2022.10

zbMATH Keywords

choice sequencesclassical logicconstructive type theoryextensional type theoryintuitionismrealizabilityreferencestheorem proving

Mathematics Subject Classification ID

Type theory (03B38) Modal logic (including the logic of norms) (03B45) Metamathematics of constructive systems (03F50)

Recommendations

• Multimodal dependent type theory
• Constructive sheaf models of type theory
• Multimodal dependent type theory
• scientific article; zbMATH DE number 1746890
• Three extensional models of type theory

Cited in

(2)

• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• Separating Markov's principles

This page was built for publication: Constructing unprejudiced extensional type theories with choices via modalities

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