See symmetry book definition 2.24.1

isFinSet(X) is a proposition and equivalent to . See symmetry book lemma 2.24.4

We define the groupoid of finite sets as

and the groupoid of sets with cardinality by

By Lemma 2.24.4 we get that

Given a group , a -set is a function .

Any paths in gives us a map that we call the group action of .

The groupoid of finite sets with cardinality , is pointed connected with base point . Its loop space is the symmetric group .

In other words

Proof. TODO.

A species is a function , where is the groupoid of finite sets and bijections.

Consider a species . By this and by this, restricts to

In other words, is given precisely by what is does on each , since

Given a path in , any type family gives a transport map

In particular for we have . So becomes an -set (see G-set) with the action

Given for a fix , the total space is by definition what we call the action type . Its objects are pairs of the form , with

See also definition 5.4.1 in the symmetry book. The action type corresponds to what we call the action groupoid or weak quotient in category theory. We will see in a second that paths in the identity type of the action type correspond precisely to the morphisms in the the action groupoid

As a Sigma-Type, the identity type of the total space is given by

, since (by definition), this is

So an element of the identity type is an element together with a proof that , which is exacly what we would expect from a morphism in the action groupoid.

Putting all of the above together we get that

In words: The total space of a species splits into components by cardinality and the n-th component is precisely the action type .