blob: be9226199b38288555b043d2615c9d129cbd5275 (
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
107
108
109
110
111
112
113
114
115
116
|
{-# OPTIONS --without-K --safe #-}
module Functor.Instance.Nat.Push where
open import Level using (0ℓ)
open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
open import Categories.Category.Instance.Nat using (Nat)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
open import Data.Circuit.Value using (monoid)
open import Data.Fin using (Fin)
open import Data.Fin.Preimage using (preimage; preimage-cong₁)
open import Data.Nat using (ℕ)
open import Data.Setoid using (∣_∣; _⇒ₛ_)
open import Data.Subset.Functional using (⁅_⁆)
open import Data.Values monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂; lookup)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)
open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
open Func
open Functor
open Object using (Valuesₘ)
private
variable A B C : ℕ
-- Push sends a natural number n to Values n
Push₀ : ℕ → CommutativeMonoid
Push₀ n = Valuesₘ n
-- action of Push on morphisms (covariant)
opaque
unfolding Values
open CommutativeMonoid using (Carrier)
open CommutativeMonoid⇒ using (arr)
-- setoid morphism
Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B
Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆
Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y
private opaque
unfolding Pushₛ _⊕_
Push-⊕
: (f : Fin A → Fin B)
→ (xs ys : ∣ Values A ∣)
→ Pushₛ f ⟨$⟩ (xs ⊕ ys)
≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys)
Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆)
Push-<ε>
: (f : Fin A → Fin B)
→ Pushₛ f ⟨$⟩ <ε> ≋ <ε>
Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆)
opaque
unfolding Valuesₘ ≋-isEquiv
-- monoid morphism
Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B)
Pushₘ f = record
{ monoid⇒ = record
{ arr = Pushₛ f
; preserves-μ = Push-⊕ f _ _
; preserves-η = Push-<ε> f
}
}
private opaque
unfolding Pushₘ Pushₛ push lookup
-- Push respects identity
Push-identity
: (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A)))
→ arr (Pushₘ id) ≈ Id (Carrier (Push₀ A))
Push-identity {_} {v} i = merge-⁅⁆ v i
-- Push respects composition
Push-homomorphism
: {f : Fin A → Fin B}
{g : Fin B → Fin C}
→ (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C)))
→ arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f)
Push-homomorphism {f = f} {g} {v} = merge-push f g v
-- Push respects equality
Push-resp-≈
: {f g : Fin A → Fin B}
→ f ≗ g
→ (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B)))
→ arr (Pushₘ f) ≈ arr (Pushₘ g)
Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
-- the Push functor
Push : Functor Nat CMonoids
Push .F₀ = Push₀
Push .F₁ = Pushₘ
Push .identity = Push-identity
Push .homomorphism = Push-homomorphism
Push .F-resp-≈ = Push-resp-≈
module Push = Functor Push
|
