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.

@phdthesis{kidney_finiteness_2020,
  title = {Finiteness in {{Cubical Type Theory}}},
  author = {Kidney, Donnacha Ois{\'i}n},
  year = {2020},
  month = sep,
  address = {{Cork, Ireland}},
  url = {https://cora.ucc.ie/handle/10468/11338},
  urldate = {2021-05-18},
  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.},
  copyright = {https://creativecommons.org/licenses/by-sa/4.0/},
  langid = {english},
  school = {University College Cork},
  annotation = {Accepted: 2021-05-18T09:03:41Z}
}