open import GpdCont.Prelude using (Type) open import Cubical.Algebra.Group.Base module GpdCont.Delooping {ℓ} (G : Group ℓ) where open import GpdCont.Delooping.Base G public open import GpdCont.Delooping.Properties G public