« Species on FinSet and action types

Definition. G-Set [00DI]

Given a group , a -set is a function .

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

Backlinks

X([n]) is an S_n-set [00DH]

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