Show simple item record

dc.rights.licenseCC-BY-NC-ND
dc.contributor.advisorOosten, J. van
dc.contributor.authorRijke, E.M.
dc.date.accessioned2012-09-28T17:01:25Z
dc.date.available2012-09-28
dc.date.available2012-09-28T17:01:25Z
dc.date.issued2012
dc.identifier.urihttps://studenttheses.uu.nl/handle/20.500.12932/11704
dc.description.abstractThe thesis introduces homotopy type theory, which refers to a new interpretation of Martin-Löf type theory. All the main recent results, such as strong function extensionality from weak, weak extensionality from univalence, and the notion of higher inductive types including the proof that the fundamental group of the circle is the integers using univalence, are included. Along with those results, there are new results such as a type theoretical yoneda lemma and various correspondence theorems for inductively defined types including higher inductive types. My other supervisors are Andrej Bauer (University of Ljubljana) and Benno van den Berg (Utrecht)
dc.description.sponsorshipUtrecht University
dc.format.extent664878 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.titleHomotopy type theory
dc.type.contentMaster Thesis
dc.rights.accessrightsOpen Access
dc.subject.keywordstype theory, homotopy, univalence, higher inductive types
dc.subject.courseuuMathematical Sciences


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record