remove obsolete definition of homotopy groups (#725)

agda · Mar 10, 2022 · c10af3f · c10af3f
1 parent 17c2725
commit c10af3f
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 60 deletions.
diff --git a/Cubical/Data/HomotopyGroup.agda b/Cubical/Data/HomotopyGroup.agda
diff --git a/Cubical/Data/HomotopyGroup/Base.agda b/Cubical/Data/HomotopyGroup/Base.agda
diff --git a/Cubical/Experiments/Brunerie.agda b/Cubical/Experiments/Brunerie.agda
@@ -5,7 +5,6 @@ open import Cubical.Foundations.Everything
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat
 open import Cubical.Data.Int
-open import Cubical.Data.HomotopyGroup
 open import Cubical.HITs.S1
 open import Cubical.HITs.S2
 open import Cubical.HITs.S3

diff --git a/Cubical/Experiments/ZCohomologyOld/Properties.agda b/Cubical/Experiments/ZCohomologyOld/Properties.agda
@@ -32,7 +32,6 @@ open import Cubical.Data.NatMinusOne
 
 open import Cubical.HITs.Pushout
 open import Cubical.Data.Sum.Base
-open import Cubical.Data.HomotopyGroup
 
 open import Cubical.Experiments.ZCohomologyOld.KcompPrelims
 

diff --git a/Cubical/Homotopy/WedgeConnectivity.agda b/Cubical/Homotopy/WedgeConnectivity.agda
@@ -2,10 +2,8 @@
 module Cubical.Homotopy.WedgeConnectivity where
 
 open import Cubical.Foundations.Everything
-open import Cubical.Data.HomotopyGroup
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
-open import Cubical.HITs.Nullification
 open import Cubical.HITs.Susp
 open import Cubical.HITs.Truncation as Trunc
 open import Cubical.Homotopy.Connected