From type theory to setoids and back

DOI10.1017/S0960129521000189MaRDI QIDQ5889302FDO

Authors 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

extensionalityconstructive set theorysetoidsMartin-Löf type theory

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Constructing categories and setoids of setoids in type theory
• Setoid type theory -- a syntactic translation
• Publication:4944846
• Elimination of extensionality in Martin-Löf type theory
• W-types in setoids

Cites work

• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1302063 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 2247253 (Why is no real title available?)
• A constructive examination of a Russell-style ramified type theory
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A minimalist two-level foundation for constructive mathematics
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Constructing a small category of setoids
• Constructing categories and setoids of setoids in type theory
• Elementary quotient completion
• Extensional Constructs in Intensional Type Theory
• Homotopy type theory. Univalent foundations of mathematics
• Inaccessibility in constructive set theory and type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• On equality of objects in categories in constructive type theory
• Proof-relevance of families of setoids and identity in type theory
• Propositions as [Types]
• Quotient completion for the foundation of constructive mathematics
• Setoids and universes
• Sets in Coq, Coq in Sets
• The strength of Martin-Löf type theory with a superuniverse. I
• The strength of Martin-Löf type theory with a superuniverse. II

Cited in

(6)

• Equiconsistency of the minimalist foundation with its classical version
• Setoid type theory -- a syntactic translation
• scientific article; zbMATH DE number 7444845 (Why is no real title available?)
• scientific article; zbMATH DE number 5976699 (Why is no real title available?)
• Type inference for set theory
• W-types in setoids

This page was built for publication: From type theory to setoids and back

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