blob: a430f12b7c183a1be9bf475eb38dfe713aded55d (
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 #-}
{-# OPTIONS --hidden-argument-puns #-}
open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid; Rel; IsEquivalence)
module Data.Vector.Core {c ℓ : Level} (S : Setoid c ℓ) where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Categories.Category.Instance.Nat using (Natop)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ; _+_)
open import Data.Setoid using (∣_∣)
open import Data.Vec as Vec using (Vec; lookup; tabulate)
open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
open Func
open Setoid S
open Fin
open Vec.Vec
private
variable
n A B C : ℕ
opaque
-- Vectors over the rig
Vector : ℕ → Set c
Vector = Vec ∣ S ∣
-- Pointwise equivalence of vectors
_≊_ : Rel (Vector n) (c ⊔ ℓ)
_≊_ A B = A ≋ B
-- Pointwise equivalence is an equivalence relation
≊-isEquiv : IsEquivalence (_≊_ {n})
≊-isEquiv {n} = ≋-isEquivalence n
_++_ : Vector A → Vector B → Vector (A + B)
_++_ = Vec._++_
⟨⟩ : Vector 0
⟨⟩ = []
⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩
⟨⟩-! [] = ≡.refl
⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V
⟨⟩-++ V = ≡.refl
-- A setoid of vectors for every natural number
Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
Vectorₛ n = record
{ Carrier = Vector n
; _≈_ = _≊_
; isEquivalence = ≊-isEquiv
}
module ≊ {n} = Setoid (Vectorₛ n)
infix 4 _≊_
opaque
unfolding Vector
pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B
pull f .to v = tabulate (λ i → lookup v (f i))
pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i))
pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v
pull-id {v} = ≊.reflexive (tabulate∘lookup v)
pull-∘
: {f : Fin B → Fin A}
{g : Fin C → Fin B}
{v : Vector A}
→ pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v)
pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i))))
pull-cong
: {f g : Fin B → Fin A}
→ f ≗ g
→ {v : Vector A}
→ pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v
pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i)))
-- Copying, deleting, and rearranging elements
-- of a vector according to a function on indices
-- gives a contravariant functor from Nat to Setoids
Pull : Functor Natop (Setoids c (c ⊔ ℓ))
Pull = record
{ F₀ = Vectorₛ
; F₁ = pull
; identity = pull-id
; homomorphism = pull-∘
; F-resp-≈ = pull-cong
}
|
