blob: ac3638f614e10f0b360186a09a37c6edfdf91d49 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Data.Nat using (ℕ)
open import Level using (Level; _⊔_)
-- The endofunctor in setoids sending A to Matrix A n m for fixed n and m
module Data.Matrix.Endofunctor (n m : ℕ) {c ℓ : Level} where
import Data.Vector.Endofunctor.Setoid as Vector
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor; _∘F_)
open import Data.Matrix.Raw as Raw using (map; map₂)
open import Data.Matrix.Core as Core using (Matrix; Matrixₛ)
open import Data.Vector.Core using (Vector)
open import Function using (_⟶ₛ_; _⟨$⟩_; Func)
open import Function.Construct.Composition using () renaming (function to compose)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (setoid)
open import Relation.Binary using (Setoid)
private
Vec∘Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
Vec∘Vec = Vector.Vec m ∘F Vector.Vec n
module Vec∘Vec = Functor Vec∘Vec
open Func
opaque
unfolding Core._≋_
mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m
to (mapₛ f) = map (to f)
cong (mapₛ f) = map₂ (cong f)
abstract opaque
unfolding mapₛ
identity
: {A : Setoid c ℓ}
{M : Matrix A n m}
(open Core A using (_≋_))
→ mapₛ (Id A) ⟨$⟩ M ≋ M
identity {A} = Vec∘Vec.identity {A}
homomorphism
: {X Y Z : Setoid c ℓ}
{f : X ⟶ₛ Y}
{g : Y ⟶ₛ Z}
{M : Matrix X n m}
(open Core Z using (_≋_))
→ mapₛ (compose f g) ⟨$⟩ M ≋ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ M)
homomorphism {f = f} {g} = Vec∘Vec.homomorphism {f = f} {g}
F-resp-≈
: {A B : Setoid c ℓ}
{f g : A ⟶ₛ B}
(open Setoid (setoid A B))
→ (f ≈ g)
→ {M : Matrix A n m}
(open Core B using (_≋_))
→ mapₛ f ⟨$⟩ M ≋ mapₛ g ⟨$⟩ M
F-resp-≈ {f = f} {g} = Vec∘Vec.F-resp-≈ {f = f} {g}
-- only a true endofunctor when c ≤ ℓ
Mat : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
Mat = record
{ F₀ = λ A → Matrixₛ A n m
; F₁ = mapₛ
; identity = identity
; homomorphism = homomorphism
; F-resp-≈ = F-resp-≈
}
|
