Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

IsMonoid instance for mod-n multiplication

  • Loading branch information...
commit 417081be33770453eef073e08480c37baa72fa18 1 parent 5494de2
Dr. Gergő Érdi authored April 24, 2012

Showing 1 changed file with 24 additions and 0 deletions. Show diff stats Hide diff stats

  1. 24  Data/Mod.agda
24  Data/Mod.agda
@@ -150,4 +150,28 @@ module Dummy {n : ℕ} where
150 150
         plus-comm : Commutative plus
151 151
         plus-comm = lift-comm′ plus₀ ℤ-CR.+-comm
152 152
 
  153
+    mul-isMonoid : IsMonoid _≡_ mul [ + 1 ]
  154
+    mul-isMonoid = record
  155
+      { isSemigroup = isSemigroup
  156
+      ; identity = mul-identityˡ , mul-identityʳ
  157
+      }
  158
+      where
  159
+      abstract
  160
+        isSemigroup : IsSemigroup _≡_ mul
  161
+        isSemigroup = record
  162
+          { isEquivalence = isEquivalence
  163
+          ; assoc = lift-assoc′ mul₀ ℤ-CR.*-assoc
  164
+          ; ∙-cong = cong₂ mul
  165
+          }
  166
+          where
  167
+          open import Relation.Binary.PropositionalEquality
  168
+
  169
+        mul-identityˡ : LeftIdentity [ + 1 ] mul
  170
+        mul-identityˡ = elim Mod₀ _ (λ x → [ (reflexive (proj₁ ℤ-CR.*-identity x)) ]-cong) (λ _ → P.proof-irrelevance _ _)
  171
+          where open Setoid Mod₀
  172
+
  173
+        mul-identityʳ : RightIdentity [ + 1 ] mul
  174
+        mul-identityʳ = elim Mod₀ _ (λ x → [ reflexive (proj₂ ℤ-CR.*-identity x) ]-cong) (λ _ → P.proof-irrelevance _ _)
  175
+          where open Setoid Mod₀
  176
+
153 177
 open Dummy public renaming (plus to _+_; minus to _-_; mul to _*_)

0 notes on commit 417081b

Please sign in to comment.
Something went wrong with that request. Please try again.