module Data.Fin.Finite where

Finite types🔗

This module pieces together a couple of pre-existing constructions: In terms of the standard finite sets (which are defined for natural numbers $n$ ) and deloopings of automorphism groups, we construct the type of finite types. By univalence, the space of finite types classifies maps with finite fibres.

But what does it mean for a type to be finite? A naïve first approach is to define “ $X$ is finite” to mean “ $X$ is equipped with $n : \mathbb{N}$ and $f : [n] \simeq X$ ” but this turns out to be too strong: This doesn’t just equip the type $X$ with a cardinality, but also with a choice of total order. Additionally, defined like this, the type of finite types is a set!

naïve-fin-is-set : is-set (Σ[ X ∈ Type ] Σ[ n ∈ Nat ] Fin n ≃ X)
naïve-fin-is-set = is-hlevel≃ 2 Σ-swap₂ $
  Σ-is-hlevel 2 (hlevel 2) λ x → is-prop→is-hlevel-suc {n = 1} $
    is-contr→is-prop $ Equiv-is-contr (Fin x)

That’s because, as the proof above shows, it’s equivalent to the type of natural numbers: The type $\sum_{X : \mathrm{Type}} \sum_{n : \mathbb{N}}\ [n] \simeq X$ is equivalent to the type $\sum_{n : \mathbb{N}} \sum_{X : \mathrm{Type}} [n] \simeq X\text{,}$ and univalence says (rather directly) that the sum of $[n] \simeq X$ as $X$ ranges over a universe is contractible, so we’re left with the type of natural numbers.

This simply won’t do: we want the type of finite sets to be equivalent to the (core of the) category of finite sets, where the automorphism group of $n$ has $n!$ elements, not exactly one element. What we do is appeal to a basic intuition: A groupoid is the sum over its connected components, and we have representatives for every connected component (given by the standard finite sets):

Fin-type : Type (lsuc lzero)
Fin-type = Σ[ n ∈ Nat ] BAut (Fin n)

Fin-type-is-groupoid : is-hlevel Fin-type 3
Fin-type-is-groupoid = Σ-is-hlevel 3 (hlevel 3) λ _ →
  BAut-is-hlevel (Fin _) 2 (hlevel 2)

Informed by this, we now express the correct definition of “being finite”, namely, being merely equivalent to some standard finite set. Rather than using Σ types for this, we can set up typeclass machinery for automatically deriving boring instances of finiteness, i.e. those that follow directly from the closure properties.

record Finite {ℓ} (T : Type ℓ) : Type ℓ where
  constructor fin
  field
    {cardinality} : Nat
    enumeration   : ∥ T ≃ Fin cardinality ∥

instance
  Finite-Fin : ∀ {n} → Finite (Fin n)
  Finite-⊎ : ⦃ Finite A ⦄ → ⦃ Finite B ⦄ → Finite (A ⊎ B)

  Finite-Σ
    : {P : A → Type ℓ} → ⦃ Finite A ⦄ → ⦃ ∀ {x} → Finite (P x) ⦄ → Finite (Σ A P)
  Finite-Π
    : {P : A → Type ℓ} → ⦃ Finite A ⦄ → ⦃ ∀ {x} → Finite (P x) ⦄ → Finite (∀ x → P x)

  Finite-⊥ : Finite ⊥
  Finite-⊤ : Finite ⊤
  Finite-Bool : Finite Bool

  Finite-PathP
    : ∀ {A : I → Type ℓ} ⦃ s : Finite (A i1) ⦄ {x y}
    → Finite (PathP A x y)

  Finite-Lift : ∀ {ℓ} → ⦃ Finite A ⦄ → Finite (Lift ℓ A)