open import 1Lab.Prelude

open import Data.Dec.Base
open import Data.Power
open import Data.Fin
open import Data.Sum

module Data.Fin.Indexed where

private variable
  ℓ : Level
  T S : Type ℓ
  P Q : ℙ S

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:\mathbb{N}$ and merely admits a bijection $X\simeq [n]\text{.}$ This is weaker than asking it to be equipped with such a bijection, since it does not impose an order on $X\text{,}$ but it can still be used to transport any property of $[n]$ to $X\text{.}$ 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 $\varphi :\Omega$ determines a subset of $[1]\text{,}$ whose cardinality — either zero or one — serves as a decision for $\varphi \text{.}$ 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. $\neg \varphi \text{.}$

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]\simeq X$ to a surjection $[n]\twoheadrightarrow X\text{,}$ we recover closure under quotients. These are the finitely-indexed types, also known as $K\text{-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:\mathbb{N}$ and the surjection $[n]\to X\text{:}$ a finite cover of $X\text{.}$

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)

{-# INLINE covering #-}

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\to \Omega$ with finitely-indexed total space $K\text{-finite}$.

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]\equiv T$ can be weakened to a $f:[n]\twoheadrightarrow T\text{,}$ 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\to \Omega$ is finitely-indexed if its total space ${\Sigma }_{x:T}x\in P$ is. To disambiguate and keep names short, we refer to types as finitely-indexed, but to subsets as K-finite.

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

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

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\cup Q\text{,}$ since we can’t decide whether or not $P$ and $Q$ have some intersection — and we have placed no such assumption on $A\text{.}$ That’s why $K\text{-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\to \Omega )\to \mathbb{N}\text{,}$ then we would have the familiar formula

Even though we don’t, if $a$ and $b$ are upper bounds for the size of $A$ and $B$ (i.e. $n(A)\le a$ and $n(B)\le B\text{),}$ then we certainly have $n(A\cup B)\le a+b\text{.}$ 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\text{-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 = } (λ _ → x , inc refl)
    λ (y , p) → inc (fzero , Σ-prop-path! (□-rec (t-set _ _) id p)))