Constructions of categories of setoids from proof-irrelevant families

DOI10.1007/S00153-016-0514-7zbMath1390.03013OpenAlexW2547417032WikidataQ59611793 ScholiaQ59611793MaRDI QIDQ512135

Erik Palmgren

Publication date: 24 February 2017

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

Full work available at URL: https://doi.org/10.1007/s00153-016-0514-7

zbMATH Keywords

categoryMartin-Löf type theoryproof-irrelevance

Mathematics Subject Classification ID

Embedding theorems, universal categories (18B15) Categories of sets, characterizations (18B05)

Related Items (1)

Algebras of complemented subsets

Uses Software

• Coq
• Agda

Cites Work

• 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
• Constructing categories and setoids of setoids in type theory
• Constructing a small category of setoids
• Setoids in type theory
• Extensional Constructs in Intensional Type Theory

This page was built for publication: Constructions of categories of setoids from proof-irrelevant families