1 files changed, 81 insertions, 0 deletions
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
new file mode 100644
index 0000000..b1764d9
--- /dev/null
+++ b/Functor/Instance/Nat/Pull.agda
@@ -0,0 +1,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