open import 1Lab.Prelude

open import Algebra.Group.Homotopy.BAut

open import Data.Fin.Properties
open import Data.Fin.Closure
open import Data.Fin.Base
open import Data.Nat
open import Data.Sum

open import Meta.Bind

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 ∥

open Finite ⦃ ... ⦄ public

instance
Finite-Fin : ∀ {n} → Finite (Fin n)
Finite-× : ⦃ Finite A ⦄ → ⦃ Finite B ⦄ → Finite (A × B)
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)