Finiteness in cubical type theory

Thumbnail Image
Files
masters-thesis.pdf(764.17 KB)
Full Text E-thesis
Date
2020-09
Authors
Kidney, Donnacha Oisín
Journal Title
Journal ISSN
Volume Title
Publisher
University College Cork
Published Version
Research Projects
Organizational Units
Journal Issue
Abstract
This thesis will explore and explain finiteness in constructive mathematics: using this setting, it will also serve as an introduction to constructive mathematics in Cubical Agda, and some related topics.
Description
Keywords
Agda , Haskell , Homotopy type theory , Automated proof assistants , Cubical type theory , Dependent type , Constructive mathematics , Topos theory , Automated theorem proving
Citation
Kidney, D. O. 2020. Finiteness in cubical type theory MRes Thesis, University College Cork.
URI
https://hdl.handle.net/10468/11338
Collections
Research Theses Submission
College of Science, Engineering and Food Science - Masters by Research Theses
Computer Science - Masters by Research Theses
Copyright
© 2020, Donnacha Oisín Kidney.