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)