Skip to content

Commit

Permalink
Workaround for Agda 2.7.0 (and lower, I suppose)
Browse files Browse the repository at this point in the history
  • Loading branch information
andreasabel committed Jan 13, 2025
1 parent 2ffb002 commit 178af29
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Algebra/Construct/Initial.agda
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ isEquivalence : IsEquivalence _≈_
isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} trans {k = k} }

isMagma : IsMagma _≈_ _∙_
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} }

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

0 comments on commit 178af29

Please sign in to comment.