{-# OPTIONS --cubical #-} -- -- Delooping with presented Eilenberg-MacLane spaces. -- open import EM -- -- Delooping with generated G-torsors. -- -- Actions of groups (G-sets) open import GSet -- Properties of G-sets open import GSetProperties -- Morphisms of G-sets open import GSetHom -- Actions of sets (X-sets) open import XSet -- Properties of X-sets open import XSetProperties -- Connected components open import Comp -- Generators for groups open import Generators -- The principal torsor open import PrincipalTorsor -- Delooping by (generated) torsors open import Deloopings -- -- Cayley graphs -- open import Cayley