Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On Constructive Sets and Partial Structures
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics, Algebra, Geometry and Logic.
2011 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The first three papers in this thesis study the formalisation of a set in type theory as a data type with an equivalence relation – an object usually known as a setoid. The corresponding formalisation of a locally small category is called an E-category.

In Paper I, we show that type theory without universes is insufficient for proving that some expected properties hold of the E-category of setoids, but that a minimal universe is sufficient.

In Paper II, we show that although the collection of all E-categories does not form a category, we can introduce a type-theoretic version of bicategories, and the E-categories form such an E-bicategory.

In Paper III, we consider the setoids inside a type-theoretic universe. The axiom of unique substitutions is proposed and used to show that these form a small category (that is, a category witha setoid of objects and a single setoid of all arrows). We demonstrate that this construction can not be carried out without adding some new axiom to type theory. We also show that the axiom of unique substitutions is strictly weaker than the axiom of unique identity proofs.

In Paper IV, we investigate partial equivalence relations, also known as partial setoids, in Heyting arithmetic in all finite types, and adapt the result that the extensional axiom of choice is equivalent to the combination of the intensional axiom of choice, classical logic, and an extensionality axiom.

In Paper V, we investigate PHL, a logic of partial terms, and prove a cut elimination theorem for it and for a related calculus.

Place, publisher, year, edition, pages
Uppsala: Department of Mathematics , 2011. , 33 p.
Series
Uppsala Dissertations in Mathematics, ISSN 1401-2049 ; 74
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:uu:diva-160605ISBN: 978-91-506-2245-4 (print)OAI: oai:DiVA.org:uu-160605DiVA: diva2:451872
Public defence
2011-12-13, Polhemsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2011-11-22 Created: 2011-10-27 Last updated: 2011-12-15Bibliographically approved
List of papers
1. Setoids and universes
Open this publication in new window or tab >>Setoids and universes
2010 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 20, no 4, 563-576 p.Article in journal (Refereed) Published
Abstract [en]

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.

National Category
Mathematics
Identifiers
urn:nbn:se:uu:diva-135600 (URN)10.1017/S0960129510000071 (DOI)000280672800003 ()
Available from: 2010-12-07 Created: 2010-12-07 Last updated: 2017-12-11Bibliographically approved
2. An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories
Open this publication in new window or tab >>An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories
2005 (English)Report (Other academic)
Series
UUDM, 2005:48
National Category
Mathematics
Identifiers
urn:nbn:se:uu:diva-77927 (URN)
Available from: 2006-03-16 Created: 2006-03-16 Last updated: 2011-12-15Bibliographically approved
3. Constructing a small category of setoids
Open this publication in new window or tab >>Constructing a small category of setoids
2012 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 22, no 1, 103-121 p.Article in journal (Refereed) Published
Abstract [en]

Consider the first-order theory of a category.  It has a sort of objects, and a sort of arrows (so we may think of it as a small category).  We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory.  We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.

National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
urn:nbn:se:uu:diva-160604 (URN)10.1017/S0960129511000478 (DOI)000299654600005 ()
Available from: 2011-10-27 Created: 2011-10-27 Last updated: 2017-12-08Bibliographically approved
4. PERs in HAω I: Basic constructions and choice principles
Open this publication in new window or tab >>PERs in HAω I: Basic constructions and choice principles
2011 (English)Report (Other academic)
Abstract [en]

We study the approximation of sets by partial equivalence rela-tions (PERs) in HAω - this construction is usually considered in type theory.In this rst part, we start with the basic denitions, and introduce notions ofequality, inclusion, and quotients of PERs. We then show that PERs form anitely complete and nitely cocomplete category, with all constructions given.We also make a detailed investigation of extensional choice principles.

Publisher
35 p.
Series
U.U.D.M. report / Uppsala University, Department of Mathematics, ISSN 1101-3591 ; 2011:17
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
urn:nbn:se:uu:diva-159876 (URN)
Available from: 2011-10-11 Created: 2011-10-11 Last updated: 2012-02-16Bibliographically approved
5. Some proof-theoretic properties of PHL and related systems
Open this publication in new window or tab >>Some proof-theoretic properties of PHL and related systems
2010 (English)Report (Other academic)
Series
U.U.D.M. report / Uppsala University, Department of Mathematics, ISSN 1101-3591 ; 2010:18
National Category
Mathematics
Identifiers
urn:nbn:se:uu:diva-135771 (URN)
Available from: 2010-12-08 Created: 2010-12-08 Last updated: 2011-12-15Bibliographically approved

Open Access in DiVA

fulltext(1233 kB)379 downloads
File information
File name FULLTEXT01.pdfFile size 1233 kBChecksum SHA-512
e7c8ea68710237dd718bf9dd1da9410df8a97131c4d937d27cf18516fd1dd81be6b377010ce9c32292b3482eac628b9fcd0adbbf0550cd3b70e37651b1c80943
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Wilander, Olov
By organisation
Algebra, Geometry and Logic
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
Total: 379 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 826 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf