Variations on Noetherianness

Denis Firsov, Tarmo Uustalu, Niccolò Veltri



In type theory several inequivalent notions of finiteness exist. In this paper we continue the study of Noetherian sets in the dependently typed setting of Agda programming language. A set is Noetherian if whenever we are shown elements from it one after another, sooner or later we will have seen some element twice. In a dependently typed setting this idea can be encoded in different ways. We explore properties and connections among various representations. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally we explore the relation between Noetherianness and other notions of finiteness.


[pdf, code (Agda; standard library 0.9)]