« Species on FinSet and action types

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

Backlinks

Identity type of the total space [00DK]

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.