open import Cat.Prelude

open import Data.Fin

module Cat.Instances.FinSet where

The category of finite sets🔗

Throughout this page, let $n$ be a natural number and $[n]$ denote the standard $n\text{-element}$ ordinal. The category of finite sets, $\mathbf{FinSets}\text{,}$ is the category with set of objects $\mathbb{N}$ the natural numbers, with set of maps $\mathbf{Hom}(j,k)$ the set of functions $[j]\to [k]\text{.}$ This category is not univalent, but it is weakly equivalent to the full subcategory of $\mathbf{Sets}$ on those objects which are merely isomorphic to a finite ordinal. The reason for this “skeletal” definition is that $\mathbf{FinSets}$ is a small category, so that presheaves on $\mathbf{FinSets}$ are a Grothendieck topos.

FinSets : Precategory lzero lzero
FinSets .Precategory.Ob = Nat
FinSets .Precategory.Hom j k = Fin j → Fin k
FinSets .Precategory.Hom-set x y = hlevel 
FinSets .Precategory.id x = x
FinSets .Precategory._∘_ f g x = f (g x)
FinSets .Precategory.idr f = refl
FinSets .Precategory.idl f = refl
FinSets .Precategory.assoc f g h = refl