« Root

Definition. Group [00DL]

TODO group in HoTT.

Backlinks

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 .