Finiteness in cubical type theory
Kidney, Donnacha Oisín
University College Cork
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.
Agda , Haskell , Homotopy type theory , Automated proof assistants , Cubical type theory , Dependent type , Constructive mathematics , Topos theory , Automated theorem proving
Kidney, D. O. 2020. Finiteness in cubical type theory MRes Thesis, University College Cork.