module Data.Fin.Indexed where

# Finitely-indexed sets🔗

Constructively, finiteness
is a fairly strong condition to impose on a type. To say that a type
$X$
has a cardinality is to say it is equipped with
$n:N$
and merely admits a
bijection
$X≃[n].$
This is weaker than asking it to be *equipped with* such a
bijection, since it does not impose an order on
$X,$
but it can still be used to transport any property of
$[n]$
to
$X.$
For example, any finite type is discrete.

The strength of finiteness means that it lacks several closure
properties that are familiar from classical mathematics, the most
shocking being that *subsets of a finite set need not be finite*.
This is because every
$ϕ:Ω$
determines a subset of
$[1],$
whose cardinality — either zero or one — serves as a decision for
$ϕ.$
Since it’s not possible to decide arbitrary propositions, we can not
assign a cardinality to arbitrary subsets. They are not closed under quotients either: we may
quotient the set
$0,1$
by the relation

and this quotient has cardinality $2$ iff. $¬ϕ.$

To recover these closure properties, we may either weaken the
construction we wish to close under — for example, limiting ourselves to
the *decidable* subsets or quotients — or we may weaken the
definition of finite, asking only that the type have a cardinality
bounded above by some natural number.

If we weaken the equivalence
$[n]≃X$
to a surjection
$[n]↠X,$
we recover closure under quotients. These are the
**finitely-indexed types**, also known as
$K-finite$
types, after the mathematician Kuratowski.

To simplify the formalisation, we will stratify the definition of
finitely-indexed by introducing a name for the intermediate data of the
cardinality
$n:N$
and the surjection
$[n]→X:$
a **finite cover** of
$X.$

record Finite-cover {ℓ} (A : Type ℓ) : Type ℓ where constructor covering field {cardinality} : Nat cover : Fin cardinality → A is-cover : is-surjective cover is-finitely-indexed : ∀ {ℓ} → Type ℓ → Type is-finitely-indexed T = □ (Finite-cover T) is-K-finite : (T → Ω) → Type is-K-finite P = is-finitely-indexed (∫ₚ P)

We will use the terminology **finitely-indexed** to
refer to types. However, it’s also convenient to have a name for this
notion applied to *subtypes*. We will call a predicate
$P:X→Ω$
with finitely-indexed total space
**$K-finite$**.

Types are **finitely indexed** when they are merely finitely covered, and
subtypes are K-finite when their total space is finitely-indexed.

## Closure properties🔗

As mentioned above, the key property that distinguishes the finitely-indexed types from the finite sets is that the former are closed under arbitrary quotients.

surjection→finite-cover : S ↠ T → Finite-cover S → Finite-cover T surjection→finite-cover (f , surj) (covering g surj') = covering (f ∘ g) (∘-is-surjective surj surj') surjection→is-finitely-indexed : S ↠ T → is-finitely-indexed S → is-finitely-indexed T surjection→is-finitely-indexed f = map (surjection→finite-cover f)

Moreover, since any $f:[n]≡T$ can be weakened to a $f:[n]↠T,$ any finite type is finitely-indexed, too.

Finite→is-finitely-indexed : ⦃ _ : Finite T ⦄ → is-finitely-indexed T Finite→is-finitely-indexed ⦃ fin eqv ⦄ = do eqv ← tr-□ eqv pure (covering _ (is-equiv→is-surjective (Equiv.inverse eqv .snd)))

## Finitely-indexed subsets🔗

We now turn to the question of finitely-indexed *subsets*. A
subset
$P:T→Ω$
is finitely-indexed if its total space
$Σ_{x:T}x∈P$
is. To disambiguate and keep names short, we refer to types as
finitely-indexed, but to subsets as **K-finite**.

The
$K-finite$
subsets of
$T$
are a sub-join
semilattice of the power-set lattice of
$T.$
That is, the empty subset is
$K-finite,$
and any union is
$K-finite$
as well. Since the empty subset is *finite*, it’s also
$K-finite,$
of course.

opaque minimal-is-K-finite : is-K-finite (minimal {X = T}) minimal-is-K-finite = inc (covering {cardinality = 0} (λ ()) λ ())

But the case of unions is slightly different. Unless
$A$
is assumed to have decidable equality, we can not compute the
cardinality of the union
$P∪Q,$
since we can’t decide whether or not
$P$
and
$Q$
have some intersection — and we have placed no such assumption on
$A.$
That’s why
$K-finite$
subsets express an *upper bound* on the cardinality of a
(sub)set.

We’re justified in doing this by the following observation: If we had a magical cardinality function $n(−):(T→Ω)→N,$ then we would have the familiar formula

$n(A∪B)=(n(A)+n(B))−n(A∩B).$Even though we don’t, if $a$ and $b$ are upper bounds for the size of $A$ and $B$ (i.e. $n(A)≤a$ and $n(B)≤B),$ then we certainly have $n(A∪B)≤a+b.$ The fact that our covering might over-count is not an issue here.

union-is-K-finite : is-K-finite P → is-K-finite Q → is-K-finite (P ∪ Q) union-is-K-finite {P = P} {Q = Q} p-fin q-fin = do covering {Pn} f f-surj ← p-fin covering {Qn} g g-surj ← q-fin let cover' : (Fin Pn ⊎ Fin Qn) → ∫ₚ (P ∪ Q) cover' = λ where (inl x) → f x .fst , inc (inl (f x .snd)) (inr x) → g x .fst , inc (inr (g x .snd)) surj' : ∀ x → ∥ fibre cover' x ∥ surj' xf = (xf .snd) >>= λ where (inl p) → do (ix , p) ← f-surj (xf .fst , p) pure (inl ix , Σ-prop-path! (ap fst p)) (inr q) → do (ix , p) ← g-surj (xf .fst , q) pure (inr ix , Σ-prop-path! (ap fst p)) surjection→is-finitely-indexed (cover' , surj') Finite→is-finitely-indexed

Moreover, we have that a singleton set is $K-finite,$ as well.

singleton-is-K-finite : is-set T → (x : T) → is-K-finite (singleton x) singleton-is-K-finite t-set x = inc (covering {cardinality = 1} (λ _ → x , inc refl) λ (y , p) → inc (fzero , Σ-prop-path! (□-rec (t-set _ _) id p)))