refactor: more on Group

jamesmckinna · jamesmckinna · commit 6778d542966f · 2025-11-09T19:03:32.000Z
diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda
@@ -114,11 +114,11 @@ _/_ = group
       { isRelHomomorphism = record
         { cong = ≈⇒≋
         }
-      ; homo = λ _ _ → refl
+      ; homo = λ _ _ → Q.refl
       }
-    ; ε-homo = refl
+    ; ε-homo = Q.refl
     }
-  ; ⁻¹-homo = λ _ → refl
+  ; ⁻¹-homo = λ _ → Q.refl
   }
 
 open IsGroupHomomorphism π-isGroupHomomorphism public

Original file line number	Diff line number	Diff line change
`@@ -114,11 +114,11 @@ _/_ = group`
`114`	`114`	`{ isRelHomomorphism = record`
`115`	`115`	`{ cong = ≈⇒≋`
`116`	`116`	`}`
`117`		`- ; homo = λ _ _ → refl`
	`117`	`+ ; homo = λ _ _ → Q.refl`
`118`	`118`	`}`
`119`		`- ; ε-homo = refl`
	`119`	`+ ; ε-homo = Q.refl`
`120`	`120`	`}`
`121`		`- ; ⁻¹-homo = λ _ → refl`
	`121`	`+ ; ⁻¹-homo = λ _ → Q.refl`
`122`	`122`	`}`
`123`	`123`
`124`	`124`	`open IsGroupHomomorphism π-isGroupHomomorphism public`