Setoids and universes

DOI10.1017/S0960129510000071zbMath1204.03060OpenAlexW2130016344MaRDI QIDQ3583021

Olov Wilander

Publication date: 26 August 2010

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

Full work available at URL: https://doi.org/10.1017/s0960129510000071

zbMATH Keywords

epimorphismstype theoryLogical Frameworkdisjoint sumscategory of setoidsminimal type universe

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

Related Items (max. 100)

From type theory to setoids and back ⋮ EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS ⋮ Category theoretic structure of setoids

Cites Work

• Unnamed Item
• Unnamed Item
• Propositional functions and families of types
• A minimalist two-level foundation for constructive mathematics
• Introduction to extensive and distributive categories
• A course in constructive algebra
• Some free constructions in realizability and proof theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• A proof-irrelevant model of Martin-Löf's logical framework

This page was built for publication: Setoids and universes