On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes
This thesis is composed of three separate parts. The first part deals with definability and productivity issues of equational systems defining polymorphic stream functions. The main result consists of showing such systems composed of only unary stream functions complete with respect to specifying c...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2015
|
| Online Access: | https://eprints.nottingham.ac.uk/28111/ |
| _version_ | 1848793509092392960 |
|---|---|
| author | Sattler, Christian |
| author_facet | Sattler, Christian |
| author_sort | Sattler, Christian |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | This thesis is composed of three separate parts.
The first part deals with definability and productivity issues of equational systems defining polymorphic stream functions. The main result consists of showing such systems composed of only unary stream functions complete with respect to specifying computable unary polymorphic stream functions.
The second part deals with syntactic and semantic notions of isomorphism of finitary inductive types and associated decidability issues. We show isomorphism of so-called guarded types decidable in the set and syntactic model, verifying that the answers coincide.
The third part deals with homotopy levels of hierarchical univalent universes in homotopy type theory, showing that the n-th universe of n-types has truncation level strictly n+1. |
| first_indexed | 2025-11-14T19:01:25Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-28111 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:01:25Z |
| publishDate | 2015 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-281112025-02-28T11:33:07Z https://eprints.nottingham.ac.uk/28111/ On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes Sattler, Christian This thesis is composed of three separate parts. The first part deals with definability and productivity issues of equational systems defining polymorphic stream functions. The main result consists of showing such systems composed of only unary stream functions complete with respect to specifying computable unary polymorphic stream functions. The second part deals with syntactic and semantic notions of isomorphism of finitary inductive types and associated decidability issues. We show isomorphism of so-called guarded types decidable in the set and syntactic model, verifying that the answers coincide. The third part deals with homotopy levels of hierarchical univalent universes in homotopy type theory, showing that the n-th universe of n-types has truncation level strictly n+1. 2015-03-15 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/28111/1/thesis-final.pdf Sattler, Christian (2015) On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes. PhD thesis, University of Nottingham. |
| spellingShingle | Sattler, Christian On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title | On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title_full | On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title_fullStr | On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title_full_unstemmed | On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title_short | On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| title_sort | on the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes |
| url | https://eprints.nottingham.ac.uk/28111/ |