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 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 .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