UniAgda.Categories.Examples.FiniteSets

Table of Contents

1 Prelude

2 The type of finite sets

Following this blog post, we define the property of some type \(A\) being finite as the propositional truncation of there existing some \(n\) such that \(A \simeq \operatorname{Fin} n\).

isFinite :  {i}
           (A : Type i)
            Type i
isFinite A =  (Σ[ n   ] (A  Fin n)) 

We then define the type of finite sets to be the appropriate \(\Sigma\)-type.

Fin-set :  (i)
           Type (lsuc i)
Fin-set i = Σ[ A  (Type i) ] isFinite A

If a type \(A\) is a finite set, then it is indeed a set.

finite-sets-are-sets :  {i} (A : Fin-set i)
                        isSet (pr₁ A)
finite-sets-are-sets (A , X) =
  Ptrunc-rec
    (isSet-is-prop A)
     { (n , f)  equiv-with-set (f ^ᵉ) (Fin-n-is-set n)})
    X

3 The precategory of finite sets

Author: James Leslie

Created: 2021-03-27 Sat 10:47