agda/agda#7674 eta-expand fields in record expression

Agda PR #7674 requires some implicit arguments explicitly in some record
expression given since variance info got refined (invariant to
non-variant) and hence solutions are no longer unique.

Author: andreasabel

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 = λ () }