From type theory to setoids and back

DOI10.1017/S0960129521000189MaRDI QIDQ5889302FDOQ5889302

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)

Cites Work

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

Cited In (6)

• Setoid type theory -- a syntactic translation
• Type inference for set theory
• W-types in setoids
• Title not available (Why is that?)
• Equiconsistency of the minimalist foundation with its classical version
• Title not available (Why is that?)

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)