module Cat.Instances.FinSet where
The category of finite setsπ
Throughout this page, let be a natural number and denote the standard -element ordinal. The category of finite sets, , is the category with set of objects the natural numbers, with set of maps the set of functions . This category is not univalent, but it is weakly equivalent to the full subcategory of on those objects which are merely isomorphic to a finite ordinal. The reason for this βskeletalβ definition is that is a small category, so that presheaves on 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