We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent fbc01da commit 5db9ac8Copy full SHA for 5db9ac8
src/Algebra/Properties/Monoid/Reasoning.agda
@@ -11,8 +11,6 @@ open import Algebra.Bundles using (Monoid)
11
12
module Algebra.Properties.Monoid.Reasoning {o ℓ} (M : Monoid o ℓ) where
13
14
-open import Algebra.Structures using (IsMagma)
15
-
16
open Monoid M
17
using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
18
; identityʳ ; ∙-cong; refl; assoc; ∙-congˡ; ∙-congʳ; trans)
@@ -51,7 +49,7 @@ open IntroElim public
51
49
52
50
module Cancellers {a b c : Carrier} (inv : a ∙ c ≈ ε) where
53
54
- cancelʳ : (b ∙ a) ∙ c ≈ b
+ cancelʳ : (b ∙ a) ∙ c ≈ b
55
cancelʳ = trans (assoc b a c) (trans (∙-congˡ inv) (identityʳ b))
56
57
cancelˡ : a ∙ (c ∙ b) ≈ b
0 commit comments