Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-05T13:11:23.976Z Has data issue: false hasContentIssue false
  • English
  • Français

Setoids and universes

Published online by Cambridge University Press:  07 April 2010

OLOV WILANDER
OLOV WILANDER*
Affiliation:
Department of Mathematics, Uppsala University, P.O. Box 480, SE-751 06 Uppsala, Sweden Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as small as possible (and thus, the type theory is as weak as possible). In particular, we will consider epimorphisms and disjoint sums. We show that, given the minimal type universe, all epimorphisms are surjections, and disjoint sums exist. Further, without universes, there are countermodels for these statements, and if we use the Logical Framework formulation of type theory, these statements are provably non-derivable.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 20 , Issue 4 , August 2010 , pp. 563 - 576
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Bishop, E. (1967) Foundations of constructive analysis, McGraw-Hill.Google Scholar
Bishop, E. and Bridges, D. (1985) Constructive analysis, Grundlehren der Mathematischen Wissenschaften 279.CrossRefGoogle Scholar
Carboni, A. (1995) Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103 (2)117–148.CrossRefGoogle Scholar
Carboni, A., Lack, S. and Walters, R. F. C. (1993) Introduction to extensive and distributive categories. J. Pure Appl. Algebra 84 (2)145–158.CrossRefGoogle Scholar
Coquand, T., Dybjer, P., Palmgren, E. and Setzer, A. (2005) Type-theoretic foundations of constructive mathematics (draft). Notes distributed at the 2005 TYPES Summer School, Göteborg, Sweden.Google Scholar
Fridlender, D. (2002) A proof-irrelevant model of Martin-Löf's logical framework. Mathematical Structures in Computer Science 12 (6)771–795.CrossRefGoogle Scholar
Maietti, M. E. (1998) The type theory of categorical universes, Ph.D. thesis, Università degli studi di Padova, Padua, Italy.Google Scholar
Maietti, M. E. (2005) Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science 15 (6)1089–1149.CrossRefGoogle Scholar
Maietti, M. E. (2007) Quotients over minimal type theory. In: Cooper, S. B., Löwe, B. and Sorbi, A. (eds.) Computation and logic in the real world, third conference on computability in Europe, CiE 2007. Springer-Verlag Lecture Notes in Computer Science 4497 517–531.CrossRefGoogle Scholar
Maietti, M. E. (2009) A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160 (3)319–354.CrossRefGoogle Scholar
Martin-Löf, P. (1984) Intuitionistic type theory: Notes by Giovanni Sambin of a Series of Lectures Given in Padua, June 1980, Studies in Proof Theory, Lecture Notes, volume 1, Bibliopolis.Google Scholar
Mines, R., Richman, F. and Ruitenburg, W. (1988) A course in constructive algebra, Universitext, Springer-Verlag.CrossRefGoogle Scholar
Nederpelt, R. P., Geuvers, J. H. and van Daalen, D. T. (eds.) Selected papers on Automath. Studies in Logic and the Foundations of Mathematics 133, North-Holland.Google Scholar
Nordström, B., Petersson, K. and Smith, J. M. (1990) Programming in Martin-Löf's type theory, International Series of Monographs on Computer Science 7, The Clarendon Press.Google Scholar
Nordström, B., Petersson, K. and Smith, J. M. (2000) Martin-Löf's type theory. In: Handbook of logic in computer science 5, Oxford University Press 1–37.Google Scholar
Smith, J. M. (1988) The independence of Peano's fourth axiom from Martin-Löf's type theory without universes. J. Symbolic Logic 53 (3)840–845.CrossRefGoogle Scholar
Smith, J. M. (1989) Propositional functions and families of types. Notre Dame J. Formal Logic 30 (3)442–458.CrossRefGoogle Scholar