Finiteness in cubical type theory
Loading...
Files
Full Text E-thesis
Date
2020-09
Authors
Kidney, Donnacha Oisín
Journal Title
Journal ISSN
Volume Title
Publisher
University College Cork
Published Version
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.