(University College Cork, 2020-09) Kidney, Donnacha Oisín; Provan, Gregory; Wu, Nicolas; Science Foundation Ireland
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.