blob: c002676cf2c6b3824e4a860b1903066103f0c3ad (
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
|
{-# 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
open Setoid S
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.Vec using (Vec; lookup; tabulate; head; tail; map; _++_; replicate; zipWith)
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 Data.Vector.Raw using (module Relation)
open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
open Func
open ℕ
Vector : ℕ → Set c
Vector = Vec Carrier
private
variable
n m A B C : ℕ
-- Pointwise equivalence of vectors
_≊_ : Rel (Vector n) (c ⊔ ℓ)
_≊_ A B = A ≋ B
infix 4 _≊_
-- Pointwise equivalence is an equivalence relation
≊-isEquiv : IsEquivalence (_≊_ {n})
≊-isEquiv {n} = ≋-isEquivalence n
-- 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)
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 = λ {f = f} {g v} → pull-∘ {f = f} {g} {v}
; F-resp-≈ = pull-cong
}
module Cong where
open Relation {R = _≈_}
head-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → head V₁ ≈ head V₂
head-cong = R-head
tail-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → tail V₁ ≊ tail V₂
tail-cong = R-tail
++-cong
: {V₁ V₂ : Vector m}
{W₁ W₂ : Vector n}
→ V₁ ≊ V₂
→ W₁ ≊ W₂
→ V₁ ++ W₁ ≊ V₂ ++ W₂
++-cong = R-++
replicate-cong : {n : ℕ} {x y : Carrier} → x ≈ y → replicate n x ≋ replicate n y
replicate-cong = R-replicate
open Cong public
|
