blob: 974f672ddbad06af9b6de5532e7b8cccda1da91d (
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
|
{-# 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 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 Vec
open Fin
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
-- 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
}
|
