We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6b2cda7 commit 5c6ff27Copy full SHA for 5c6ff27
src/Algebra/Construct/Quotient/Group.agda
@@ -105,6 +105,9 @@ quotientIsGroup = record
105
quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
106
quotientGroup = record { isGroup = quotientIsGroup }
107
108
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
109
+_/_ = quotientGroup
110
+
111
project : Group.Carrier G → Group.Carrier quotientGroup
112
project x = x -- because we do all the work in the relation
113
0 commit comments