In set-based mathematics an equivalence relation can be fully characterised in terms of subset-membership into equivalence classes and partitions. This is trivial to prove on paper, but I found it less obvious to be formalised in Agda at least for my novice skills in the discipline of dependent type theory. In fact, to the trained mathematician, "proofs" after the principle of Propositions-as-Types might seem affected by a 21st-century extreme bourbakism. Nonetheless, regarded as a library, I hope the following can be reused in the formalisation of more involved combinatory results dealing with invariants of algebraic structures: the paradigmatic example here is the orbital equation from Group Theory and essential results deriving from it like Sylow Theorems. In order to formalise these facts about quotients of finite sets, we apply to the finite case more general results from Cohen and Altenkirch. The extra fun comes when trying to play-by-the-rules, that is prove these ideas reusing as much as possible existing functions from Agda standard library.
Given an equivalence relation inline_formula not implemented over a finite set inline_formula not implemented, assume we can exhibit a set of representatives inline_formula not implemented, one for each equivalence class in inline_formula not implemented, then inline_formula not implemented is the disjoint union of all classes of elements in inline_formula not implemented and inline_formula not implemented is called a transversal of inline_formula not implemented:
formula not implemented
in other terms inline_formula not implemented induces a partition on inline_formula not implemented and in particular its cardinality is additive on classes:
In the section Partitions we'll show that for all natural numbers n the type of finite decidable Setoids on n elements is "equivalent" to the type of partitions of the finite type on n elements.
Sections Subset Lemmas and List-Relations Properties contain proofs and definitions to show the above results while some boring subset helpers are relegated to the Appendix. All sections are matched with dedicated inter-depending Agda runtime.
by opening its record type, within this module FinDecEq definitions are directly available, in particular throughout the this section F denotes (the type of) the finite set with n elements. We distinguish inline_formula not implemented subset-membership from inline_formula not implemented list-membership. Please forgive the cheesy comprehension syntax for lists
First basic fact: being in relation means to belong to the same class
In particular every class is non empty as a consequence of reflexivity.
and the converse is also true
now by symmetry we have the desired equivalent formulation
Now the questions we want to answer next is how many distinct classes does an equivalence posses and do such classes partition the carrier set? Or again can we find a subset on which inline_formula not implemented is a bijection? Can we find a prescribed set of computationally well-behaved (i.e. decidable) representatives for the equivalence classes?
We first introduce a canonical choice inline_formula not implemented with the following properties:
inline_formula not implemented for all inline_formula not implemented
inline_formula not implemented if and only if inline_formula not implemented
inline_formula not implemented is idempotent
In the finite setting (as in any well ordering), given any family of nonempty sets it is possible to find a choice-function: the minimum element. In the following code we're using index and index-inline_formula not implemented functions defined in the section Subset Lemmas
A canonical representative of an inline_formula not implemented-class is the minimum element with respect to the natural order on inline_formula not implemented. This is a decidable property because the finite type has a decidable equality. As transversal of inline_formula not implementedwe can take the set of all canonical representatives constructed in this way (recall that inline_formula not implemented is the set inline_formula not implementedrepresented as a list)
for all inline_formula not implemented in inline_formula not implementedthere exists an equivalence class of a canonical representative which inline_formula not implemented belongs to:
-- AnyProps.map⁺ : Any (P ∘ f) xs → Any P (List.map f xs)
Any two distinct canonical classes are disjoint. The term filter⁺₃ used below is proven in at the end of section List-Relations Properties while for definitions of Disj and disj⇒Disj see Subset Lemmas
Now we can transpose the above results in the language of subsets finding first that the union of all canonical classes gives back the whole finite set F
and furthermore since canonical classes are disjoint
we conclude with a proof of existence for a finite choice function
Since finite sets carry a natural order we can always find the smallest element in a non empty subset. Note how Agda type checker eliminates obvious non matching patterns given we're dealing with non-empty sets only.