We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
GpdCont.Delooping
1 parent af361f2 commit e36a5a0Copy full SHA for e36a5a0
GpdCont/Group/MapConjugator.agda
@@ -1,6 +1,5 @@
1
open import GpdCont.Prelude
2
open import GpdCont.Group.DeloopingCategory
3
-import GpdCont.Delooping as Delooping
4
5
open import Cubical.Foundations.HLevels
6
open import Cubical.Foundations.Equiv
@@ -25,12 +24,6 @@ module GpdCont.Group.MapConjugator {ℓ} {G H : Group ℓ} where
25
24
private
26
open module H = GroupStr (str H) using (_·_)
27
28
- 𝔹G = Delooping.𝔹 G
29
- 𝔹H = Delooping.𝔹 H
30
-
31
- module 𝔹G = Delooping G
32
- module 𝔹H = Delooping H
33
34
variable
35
φ ψ : GroupHom G H
36
0 commit comments