open import Cat.Functor.Properties.FullyFaithful
open import Cat.Instances.Sets.Cocomplete
open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Colimit.Finite
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Properties
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Instances.Sets
open import Cat.Functor.Base
open import Cat.Skeletal
open import Cat.Prelude

open import Data.Fin.Closure
open import Data.Fin
open import Data.Nat

open Functor
module Cat.Instances.FinSets where

The category of finite sets🔗

Throughout this page, let be a natural number and denote the standard 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

The category of finite sets can be seen as a full subcategory of the category of sets via the fully faithful inclusion functor that sends to 

Fin→Sets : Functor FinSets (Sets lzero)
Fin→Sets .F₀ n = el! (Fin n)
Fin→Sets .F₁ f = f
Fin→Sets .F-id = refl
Fin→Sets .F-∘ _ _ = refl

Fin→Sets-is-ff : is-fully-faithful Fin→Sets
Fin→Sets-is-ff = id-equiv

As we said earlier, FinSets is skeletal: this follows directly from the injectivity of Fin.

FinSets-is-skeletal : is-skeletal FinSets
FinSets-is-skeletal = path-from-has-iso→is-skeletal _ $ rec! λ is →
  Fin-injective (iso→equiv (F-map-iso Fin→Sets is))

Finite limits and colimits🔗

The nice closure properties of finite sets, along with the fact that fully faithful functors reflect (co)limits, imply that the category admits finite products and coproducts, equalisers and coequalisers, making it finitely complete and finitely cocomplete.

FinSets-finitely-complete : Finitely-complete FinSets
FinSets-finitely-complete = with-equalisers _ terminal products equalisers where
  terminal : Terminal FinSets
  terminal = ff→reflects-Terminal Fin→Sets Fin→Sets-is-ff
    Sets-terminal
    (equiv→iso (is-contr→≃ (hlevel 0) Finite-one-is-contr))

  products : has-products FinSets
  products a b = ff→reflects-Product Fin→Sets Fin→Sets-is-ff
    (Sets-products _ _)
    (equiv→iso Finite-multiply)

  equalisers : has-equalisers FinSets
  equalisers f g = ff→reflects-Equaliser Fin→Sets Fin→Sets-is-ff
    (Sets-equalisers f g)
    (equiv→iso (Finite-subset (λ x → f x ≡ g x) .snd e⁻Âč))

FinSets-finitely-cocomplete : Finitely-cocomplete FinSets
FinSets-finitely-cocomplete = with-coequalisers _ initial coproducts coequalisers where
  initial : Initial FinSets
  initial = ff→reflects-Initial Fin→Sets Fin→Sets-is-ff
    Sets-initial
    (equiv→iso (Lift-≃ ∙e Finite-zero-is-initial e⁻Âč))

  coproducts : has-coproducts FinSets
  coproducts a b = ff→reflects-Coproduct Fin→Sets Fin→Sets-is-ff
    (Sets-coproducts _ _)
    (equiv→iso Finite-coproduct)

  coequalisers : has-coequalisers FinSets
  coequalisers f g = ff→reflects-Coequaliser Fin→Sets Fin→Sets-is-ff
    (Sets-coequalisers f g)
    (equiv→iso (Finite-coequaliser f g .snd e⁻Âč))