module Data.Fin.Finite.Listed where

# Finite types through lists🔗

We have defined finiteness (and finite indexing) for a type $T$ in terms of its relationship with a specific standard finite set $[n].$ However, this is not always the most convenient presentation of finiteness. It’s often desirable to have an actual list of $T’s$ purported elements, which can be manipulated using the usual toolkit for working on lists.

To this end, we define a **listing** for a type
$A$
to consist of a list
$members:List(A)$
which contains every element of
$A$
at least once. The type-theoretic interpretation of “contains at least
once” is up for debate: it could either mean that we have an operation
$ix(a):a∈members$
assigning each element of
$T$
to its index in
$members,$
or that we have the weaker
$ix(a):∥a∈members∥,$
which only merely gets us
an index.

record Listing {ℓ} (A : Type ℓ) : Type ℓ where field members : List A has-member : ∀ a → ∥ a ∈ₗ members ∥

Our choice is the latter, and the reason is twofold: First, this
corresponds directly to the notion of finite cover, which means that
*having a listing* will be equivalent to *being finitely
indexed*, as desired.

listing→finite-cover : Listing A → Finite-cover A listing→finite-cover l = record { cover = l .members !_ ; is-cover = λ x → element→!-fibre <$> l .has-member x } finite-cover→listing : Finite-cover A → Listing A finite-cover→listing (covering f has) = record { members = tabulate f ; has-member = λ a → Equiv.from (member-tabulate f a) <$> has a }

The second motivation has to do with *identity* of listings:
we want to regard listings as the same precisely when their underlying
lists are the same. However, if the assignment of indices were not
truncated, it would also factor identity of listings: we could regard
$[0,0]$
as a listing for the unit type in two different ways, depending on
whether we give back the index 0 or the index 1.

## Enumerations🔗

Refining the notion of listing, we have
**enumerations**: in a listing, each element appears at
least once, but it may appear an arbitrary number of times. In an
enumeration, each element is required to appear *exactly* once.
To state this in a coherent way, we demand that, for each
$a,$
the type of proofs-of-membership
$a∈members$
be contractible.

record Enumeration {ℓ} (A : Type ℓ) : Type ℓ where field members : List A has-member : ∀ a → is-contr (a ∈ₗ members)

Unsurprisingly, much like a listing corresponds to a surjection
$[n]→A,$
an enumeration corresponds to an *equivalence*
$[n]→A.$

enumeration→fin-equiv : (l : Enumeration A) → Fin (length (l .members)) ≃ A enumeration→fin-equiv l .fst a = l .members ! a enumeration→fin-equiv l .snd .is-eqv a = Equiv→is-hlevel 0 (Equiv.inverse element≃!-fibre) (l .has-member a) fin-equiv→enumeration : ∀ {n} → Fin n ≃ A → Enumeration A fin-equiv→enumeration (fn , eqv) = record { members = tabulate fn ; has-member = λ a → Equiv→is-hlevel 0 (member-tabulate fn a) (eqv .is-eqv a) }

enumeration→finite : Enumeration A → Finite A enumeration→finite l = fin (pure (Equiv.inverse (enumeration→fin-equiv l)))

## For discrete types🔗

An important theorem about finitely-indexed sets is that, if they are discrete, then they are properly finite. This is much easier to prove when working with listings than when working with surjections, because the heavy lifting applies generically to arbitrary lists.

Given a listing, we may `nub`

the list
$xs$
of members, removing the duplicates: the resulting list
$ys$
has each
$x∈ys$
a proposition. Since each
$x∈xs$
was merely inhabited, each
$x:A$
appears both *at least* and *at most* once in
$ys:$
we have refined the listing into an enumeration.

nub-listing : ⦃ _ : Discrete A ⦄ → Listing A → Enumeration A nub-listing li = record { members = nub m ; has-member = λ a → ∥-∥-out! do memb ← has a pure (is-prop∙→is-contr (member-nub-is-prop m) (member→member-nub memb)) } where open Listing li renaming (members to m ; has-member to has)

Plugging this construction into the connections between listings and notions of finiteness constructed above, we obtain the desired theorem: a finitely-indexed discrete type is finite.

Discrete-finitely-indexed→Finite : ⦃ _ : Discrete A ⦄ → is-finitely-indexed A → Finite A Discrete-finitely-indexed→Finite fi = ∥-∥-out! do cov ← □-tr fi let over = finite-cover→listing cov exact = nub-listing over pure (enumeration→finite exact)