Proof-relevance of families of setoids and identity in type theory

DOI10.1007/s00153-011-0252-9zbMath1241.03005OpenAlexW2036690021MaRDI QIDQ661282

Erik Palmgren

Publication date: 10 February 2012

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-011-0252-9

zbMATH Keywords

Martin-Löf type theorydependent typesidentity typeproof-relevance

Mathematics Subject Classification ID

Categories of sets, characterizations (18B05)

Related Items (6)

From type theory to setoids and back ⋮ Unnamed Item ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ A generalization of the Takeuti–Gandy interpretation ⋮ W-types in setoids ⋮ Categories with families and first-order logic with dependent sorts

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A course in constructive algebra
• A coherence theorem for Martin-Löf's type theory
• The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Proof-relevance of families of setoids and identity in type theory