Skip to content

Commit b0505d6

Browse files
committed
Workaround for Agda 2.7.0 (and lower, I suppose)
1 parent 5f9de0a commit b0505d6

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Algebra/Construct/Initial.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ isEquivalence : IsEquivalence _≈_
7878
isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} trans {k = k} }
7979

8080
isMagma : IsMagma _≈_ _∙_
81-
isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {v = v} ∙-cong {y = y} {v = v} }
81+
isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {u = u} {v = v} ∙-cong {y = y} {v = v} }
8282

8383
isSemigroup : IsSemigroup _≈_ _∙_
8484
isSemigroup = record { isMagma = isMagma ; assoc = λ () }

0 commit comments

Comments
 (0)