module Cat.Instances.FinSet where

The category of finite setsπŸ”—

Throughout this page, let nn be a natural number and [n][n] denote the standard nn-element ordinal. The category of finite sets, FinSets\mathbf{FinSets}, is the category with set of objects N\mathbb{N} the natural numbers, with set of maps Hom(j,k)\mathbf{Hom}(j,k) the set of functions [j]β†’[k][j] \to [k]. This category is not univalent, but it is weakly equivalent to the full subcategory of Sets\mathbf{Sets} on those objects which are merely isomorphic to a finite ordinal. The reason for this β€œskeletal” definition is that FinSets\mathbf{FinSets} is a small category, so that presheaves on FinSets\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 2
FinSets 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