This is a small library for working with finite sets, based on some of the constructs in [1]: a set is considered finite if there's a list that can be shown to contain all of its elements. A form of the finite pigeonhole theorem is implemented in Finite.Pigeonhole: any vector of length n with elements drawn from a finite set with cardinality less than n must contain at least one element that occurs at least twice.
Building requires the Agda standard library to be installed and associated with the name standard-libarary in an Agda libraries file.
This code has been tested against Agda version 2.5.4.2 and standard library version 0.17.