From type theory to setoids and back

DOI10.1017/S0960129521000189MaRDI QIDQ5889302

Erik Palmgren

Publication date: 19 April 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1909.01414

zbMATH Keywords

extensionalityMartin-Löf type theoryconstructive set theorysetoids

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quotient completion for the foundation of constructive mathematics
• Proof-relevance of families of setoids and identity in type theory
• A minimalist two-level foundation for constructive mathematics
• Inaccessibility in constructive set theory and type theory
• The strength of Martin-Löf type theory with a superuniverse. I
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Elementary quotient completion
• Constructing categories and setoids of setoids in type theory
• Constructing a small category of setoids
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Setoids and universes
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Extensional Constructs in Intensional Type Theory
• A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY
• Propositions as [Types]
• Homotopy Type Theory: Univalent Foundations of Mathematics
• The strength of Martin-Löf type theory with a superuniverse. II