We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 9fd1ef6 commit ac03c72Copy full SHA for ac03c72
src/Algebra/Construct/Initial.agda
@@ -78,7 +78,7 @@ isEquivalence : IsEquivalence _≈_
78
isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} → trans {k = k} }
79
80
isMagma : IsMagma _≈_ _∙_
81
-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {v = v} → ∙-cong {y = y} {v = v} }
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {u = u} {v = v} → ∙-cong {y = y} {v = v} }
82
83
isSemigroup : IsSemigroup _≈_ _∙_
84
isSemigroup = record { isMagma = isMagma ; assoc = λ () }
0 commit comments