blob: 3f133036e04846f5c31e6c3eb3dca94b5cce8183 (
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
|
{-# OPTIONS --without-K --safe #-}
module Functor.Instance.Nat.Pull where
open import Categories.Category.Core using (module Category)
open import Categories.Category.Instance.Nat using (Nat)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage)
open import Data.Circuit.Value using (Value)
open import Data.Fin.Base using (Fin)
open import Data.Fin.Preimage using (preimage; preimage-cong₁)
open import Data.Nat.Base using (ℕ)
open import Data.Subset.Functional using (⁅_⁆)
open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
open import Function.Base using (id; flip; _∘_)
open import Function.Bundles using (Func; _⟶ₛ_)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (setoid; _∙_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
open Functor
open Func
module Nat = Category Nat
_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
_≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
infixr 4 _≈_
private
variable A B C : ℕ
-- action on objects (Vector Value n)
Values : ℕ → Setoid 0ℓ 0ℓ
Values = ≋-setoid (≡.setoid Value)
-- action of Pull on morphisms (contravariant)
Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A
to (Pull₁ f) i = i ∘ f
cong (Pull₁ f) x≗y = x≗y ∘ f
-- Pull respects identity
Pull-identity : Pull₁ id ≈ Id (Values A)
Pull-identity {A} = Setoid.refl (Values A)
-- Pull flips composition
Pull-homomorphism
: {A B C : ℕ}
(f : Fin A → Fin B)
(g : Fin B → Fin C)
→ Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g
Pull-homomorphism {A} _ _ = Setoid.refl (Values A)
-- Pull respects equality
Pull-resp-≈
: {f g : Fin A → Fin B}
→ f ≗ g
→ Pull₁ f ≈ Pull₁ g
Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
-- the Pull functor
Pull : Functor Nat.op (Setoids 0ℓ 0ℓ)
F₀ Pull = Values
F₁ Pull = Pull₁
identity Pull = Pull-identity
homomorphism Pull {f = f} {g} {v} = Pull-homomorphism g f {v}
F-resp-≈ Pull = Pull-resp-≈
|
