blob: b1764d9f85174ed00802d433ae21031387ca760f (
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
|
{-# OPTIONS --without-K --safe #-}
module Functor.Instance.Nat.Pull where
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.Base using (Fin)
open import Data.Nat.Base using (ℕ)
open import Function.Base using (id; _∘_)
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 import Data.Circuit.Value using (Monoid)
open import Data.System.Values Monoid using (Values)
open import Data.Unit using (⊤; tt)
open Functor
open Func
-- Pull takes a natural number n to the setoid Values n
private
variable A B C : ℕ
_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
_≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
infixr 4 _≈_
opaque
unfolding Values
-- 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)
opaque
unfolding Pull₁
-- Pull flips composition
Pull-homomorphism
: (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
opaque
unfolding Pull₁
Pull-defs : ⊤
Pull-defs = tt
-- the Pull functor
Pull : Functor Natop (Setoids 0ℓ 0ℓ)
F₀ Pull = Values
F₁ Pull = Pull₁
identity Pull = Pull-identity
homomorphism Pull {f = f} {g} = Pull-homomorphism g f
F-resp-≈ Pull = Pull-resp-≈
module Pull = Functor Pull
|
