Definition. Groupoid of finite sets FinSet [00DD]

We define the groupoid of finite sets as

and the groupoid of sets with cardinality by