blob: 217c754e082c42bd4ef137b4790385b2ae6e43ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
{-# OPTIONS --without-K --safe #-}
open import Data.Nat using (ℕ)
open import Level using (Level; _⊔_)
-- The endofunctor in monoids sending A to Vectorₘ A n for a fixed n
module Data.Vector.Endofunctor.Monoid (n : ℕ) {c ℓ : Level} where
import Data.Vec as Vec
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Algebra using (Monoid)
open import Categories.Category using (Category; _[_∘_]; _[_≈_])
open import Categories.Functor using (Functor)
open import Category.Instance.Monoids using (Monoids; MonoidHomomorphism; mk-⇒)
open import Data.Monoid using (toMonoid)
open import Data.Vec.Properties using (map-replicate)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊; replicate-cong)
open import Data.Vector.Endofunctor.Setoid as Endo using (mapₛ; zipWith-cong)
open import Data.Vector.Monoid as Mon using (Vectorₘ; ⟨ε⟩) renaming (_⊕_ to _[_⊕_])
open import Data.Vector.Vec using (map-zipWith; zipWith-map-map)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
open Func
open MonoidHomomorphism
private module _ {M N : Monoid c ℓ} (f : MonoidHomomorphism c ℓ M N) where
private
module M = Monoid M
module N = Monoid N
open Core N.setoid using (_≊_)
open ≈-Reasoning (Vectorₛ N.setoid n)
opaque
unfolding _[_⊕_]
map-⊕
: (W V : Vector M.setoid n)
→ mapₛ n (func f) ⟨$⟩ (M [ W ⊕ V ])
≊ N [ mapₛ n (func f) ⟨$⟩ W ⊕ mapₛ n (func f) ⟨$⟩ V ]
map-⊕ W V = begin
Vec.map ⟦ f ⟧ (Vec.zipWith M._∙_ W V) ≡⟨ map-zipWith ⟦ f ⟧ M._∙_ W V ⟩
Vec.zipWith (λ x y → ⟦ f ⟧ (x M.∙ y)) W V ≈⟨ zipWith-cong n N.setoid (homo f) W V ⟩
Vec.zipWith (λ x y → ⟦ f ⟧ x N.∙ ⟦ f ⟧ y) W V ≡⟨ zipWith-map-map ⟦ f ⟧ ⟦ f ⟧ N._∙_ W V ⟩
Vec.zipWith N._∙_ (Vec.map ⟦ f ⟧ W) (Vec.map ⟦ f ⟧ V) ∎
opaque
unfolding ⟨ε⟩
map-⟨ε⟩ : mapₛ n (func f) ⟨$⟩ (Mon.⟨ε⟩ M) ≊ Mon.⟨ε⟩ N
map-⟨ε⟩ = begin
Vec.map (to (func f)) (Vec.replicate n M.ε) ≡⟨ map-replicate (to (func f)) M.ε n ⟩
Vec.replicate n (func f ⟨$⟩ M.ε) ≈⟨ replicate-cong N.setoid (ε-homo f) ⟩
Vec.replicate n N.ε ∎
mapₘ : {M N : Monoid c ℓ} → MonoidHomomorphism c ℓ M N → MonoidHomomorphism c (c ⊔ ℓ) (Vectorₘ M n) (Vectorₘ N n)
mapₘ {M} {N} f = mk-⇒ record
{ ⟦_⟧ = to (mapₛ n (func f))
; isMonoidHomomorphism = record
{ isMagmaHomomorphism = record
{ isRelHomomorphism = record
{ cong = map⁺ (⟦⟧-cong f)
}
; homo = map-⊕ f
}
; ε-homo = map-⟨ε⟩ f
}
}
open Category using (id)
abstract
identity
: {A : Monoid c ℓ}
→ Monoids c (c ⊔ ℓ) [ mapₘ (id (Monoids c ℓ) {A}) ≈ id (Monoids c (c ⊔ ℓ)) ]
identity {A} V = Endo.identity n {c} {ℓ} {Monoid.setoid A}
homomorphism
: {X Y Z : Monoid c ℓ}
{f : MonoidHomomorphism c ℓ X Y}
{g : MonoidHomomorphism c ℓ Y Z}
→ Monoids c (c ⊔ ℓ) [ mapₘ (Monoids c ℓ [ g ∘ f ]) ≈ Monoids c (c ⊔ ℓ) [ mapₘ g ∘ mapₘ f ] ]
homomorphism {X} {Y} {Z} {f} {g} V = Endo.homomorphism n {c} {ℓ} {setoid X} {setoid Y} {setoid Z} {func f} {func g} {V}
where
open Monoid using (setoid)
F-resp-≈
: {A B : Monoid c ℓ}
{f g : MonoidHomomorphism c ℓ A B}
→ Monoids c ℓ [ f ≈ g ]
→ Monoids c (c ⊔ ℓ) [ mapₘ f ≈ mapₘ g ]
F-resp-≈ {A} {B} {f} {g} f≈g V = Endo.F-resp-≈ n {c} {ℓ} {setoid A} {setoid B} {func f} {func g} (λ {x} → f≈g x)
where
open Monoid using (setoid)
-- only a true endofunctor when c ≤ ℓ
Vec : Functor (Monoids c ℓ) (Monoids c (c ⊔ ℓ))
Vec = record
{ F₀ = λ M → Vectorₘ M n
; F₁ = mapₘ
; identity = λ {M} → identity {M}
; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g}
; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g}
}
|
