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 has a cardinality is to say it is equipped with and merely admits a bijection This is weaker than asking it to be equipped with such a bijection, since it does not impose an order on but it can still be used to transport any property of to 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 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 by the relation

and this quotient has cardinality 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 to a surjection we recover closure under quotients. These are the finitely-indexed types, also known as 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 and the surjection a finite cover of

record Finite-cover {} (A : Type ) : Type  where
  constructor covering
    {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 with finitely-indexed total space .


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.

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

  : S  T  is-finitely-indexed S  is-finitely-indexed T
surjection→is-finitely-indexed f = map (surjection→finite-cover f)

Moreover, since any can be weakened to a 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 is finitely-indexed if its total space is. To disambiguate and keep names short, we refer to types as finitely-indexed, but to subsets as K-finite.

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

  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 is assumed to have decidable equality, we can not compute the cardinality of the union since we can’t decide whether or not and have some intersection — and we have placed no such assumption on That’s why 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 then we would have the familiar formula

Even though we don’t, if and are upper bounds for the size of and (i.e.  and then we certainly have 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

      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 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)))