File tree Expand file tree Collapse file tree 3 files changed +6
-6
lines changed
src/Function/Endomorphism Expand file tree Collapse file tree 3 files changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -42,7 +42,7 @@ Un-deprecated modules
42
42
* The modules ` Function.Endomorphism.Propositional ` and
43
43
` Function.Endomorphism.Setoid ` previously used the old ` Function `
44
44
hierarchy but have now been ported to using the new one.
45
-
45
+
46
46
Deprecated names
47
47
----------------
48
48
@@ -186,7 +186,7 @@ Additions to existing modules
186
186
IsSemigroupMonomorphism : (A → B) → Set _
187
187
IsSemigroupIsomorphism : (A → B) → Set _
188
188
```
189
-
189
+
190
190
* In ` Algebra.Properties.Group ` :
191
191
``` agda
192
192
isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
Original file line number Diff line number Diff line change @@ -97,7 +97,7 @@ private
97
97
{ isRelHomomorphism = record { cong = cong (f ^_) }
98
98
; homo = ^-homo f
99
99
}
100
-
100
+
101
101
^-isMonoidMorphism : ∀ f → IsMonoidHomomorphism +-0-rawMonoid ∘-id-rawMonoid (f ^_)
102
102
^-isMonoidMorphism f = record
103
103
{ isMagmaHomomorphism = ^-isSemigroupMorphism f
Original file line number Diff line number Diff line change @@ -43,7 +43,7 @@ infixr 8 _^_
43
43
private
44
44
id : Endo
45
45
id = identity S
46
-
46
+
47
47
_^_ : Endo → ℕ → Endo
48
48
f ^ zero = id
49
49
f ^ suc n = f ∘ (f ^ n)
@@ -62,7 +62,7 @@ f ^ suc n = f ∘ (f ^ n)
62
62
∘-isMagma : IsMagma _≈_ _∘_
63
63
∘-isMagma = record
64
64
{ isEquivalence = isEquivalence
65
- ; ∙-cong = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
65
+ ; ∙-cong = λ {_} {_} {_} {v} x≈y u≈v → S.trans u≈v (cong v x≈y)
66
66
}
67
67
where
68
68
module S = Setoid S
@@ -94,7 +94,7 @@ private
94
94
95
95
∘-id-rawMonoid : RawMonoid (c ⊔ e) (c ⊔ e)
96
96
∘-id-rawMonoid = Monoid.rawMonoid ∘-id-monoid
97
-
97
+
98
98
------------------------------------------------------------------------
99
99
-- Homomorphism
100
100
You can’t perform that action at this time.
0 commit comments