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 ) 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 β is finiteβ to mean β is equipped with and β but this turns out to be too strong: This doesnβt just equip the type 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 is equivalent to the type and univalence says (rather directly) that the sum of as 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 has 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)