From 69b82b0f568dd840f05f6aa9902ee6dcd5df5cad Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 8 Mar 2022 18:49:39 +0000
Subject: Migrate to agda-stdlib-2.0-dev.

---
 src/Helium/Algebra/Structures.agda | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src/Helium/Algebra/Structures.agda')

diff --git a/src/Helium/Algebra/Structures.agda b/src/Helium/Algebra/Structures.agda
index b64b4c7..f88ce59 100644
--- a/src/Helium/Algebra/Structures.agda
+++ b/src/Helium/Algebra/Structures.agda
@@ -72,6 +72,7 @@ record IsDivisionRing
          (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where
   field
     +-isAbelianGroup : IsAbelianGroup + 0# -_
+    -- FIXME: unroll definition
     *-isAlmostGroup  : IsAlmostGroup _*_ 0# 1# _⁻¹
     distrib          : _*_ DistributesOver +
     zero             : Zero 0# _*_
@@ -126,7 +127,9 @@ record IsDivisionRing
   isRing : IsRing + _*_ -_ 0# 1#
   isRing = record
     { +-isAbelianGroup = +-isAbelianGroup
-    ; *-isMonoid = *-isMonoid
+    ; *-cong = *-cong
+    ; *-assoc = *-assoc
+    ; *-identity = *-identity
     ; distrib = distrib
     ; zero = zero
     }
-- 
cgit v1.2.3