On Constructive Sets and Partial Structures
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 u...
| Main Author: | |
|---|---|
| Format: | Doctoral Thesis |
| Language: | English |
| Published: |
Uppsala universitet, Algebra, geometri och logik
2011
|
| Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-160605 http://nbn-resolving.de/urn:isbn:978-91-506-2245-4 |