open import Cat.Prelude

open import Data.Fin

import Cat.Reasoning as Cat

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$-element ordinal. The category of finite sets, ${{\mathbf{FinSets}}}$, 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]$. 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 2
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