diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
index 57648d6735..411c1e580d 100644
--- a/src/Algebra/Construct/Initial.agda
+++ b/src/Algebra/Construct/Initial.agda
@@ -75,10 +75,10 @@ rawMagma = record { ℤero }
 -- Structures
 
 isEquivalence : IsEquivalence _≈_
-isEquivalence = record { ℤero }
+isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} → trans {k = k} }
 
 isMagma : IsMagma _≈_ _∙_
-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {v = v} → ∙-cong {y = y} {v = v} }
 
 isSemigroup : IsSemigroup _≈_ _∙_
 isSemigroup = record { isMagma = isMagma ; assoc = λ () }