On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes
Publication Date
March 15, 2015
Creator
Abstract
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.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
28111
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
thesis-final.pdf
Type
Full-text
Description
Examined
Size
1.37 MB
Format
Adobe PDF
Checksum (MD5)
6c715a151f984cc6eafae7d995986575