diff options
Diffstat (limited to 'Functor/Instance/Nat/Push.agda')
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 115 |
1 files changed, 76 insertions, 39 deletions
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda index 8126006..71b9a63 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -2,78 +2,115 @@ module Functor.Instance.Nat.Push where -open import Categories.Functor using (Functor) +open import Level using (0ℓ) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) + open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) -open import Data.Fin.Base using (Fin) +open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Data.Circuit.Value using (Monoid) +open import Data.Fin using (Fin) open import Data.Fin.Preimage using (preimage; preimage-cong₁) -open import Data.Nat.Base using (ℕ) +open import Data.Nat using (ℕ) +open import Data.Setoid using (∣_∣; _⇒ₛ_) open import Data.Subset.Functional using (⁅_⁆) -open import Function.Base using (id; _∘_) -open import Function.Bundles using (Func; _⟶ₛ_) +open import Data.System.Values Monoid using (Values; module Object; _⊕_; <ε>; _≋_; ≋-isEquiv; merge; push; merge-⊕; merge-<ε>; merge-cong; merge-⁅⁆; merge-push; merge-cong₂) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id) 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 Function.Construct.Setoid using (_∙_) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid; CommutativeMonoid⇒) +open import Relation.Binary using (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 Func open Functor - --- Push sends a natural number n to Values n +open Object using (Valuesₘ) private variable A B C : ℕ - _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ - _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) - infixr 4 _≈_ + -- Push sends a natural number n to Values n + Push₀ : ℕ → CommutativeMonoid + Push₀ n = Valuesₘ n + + -- action of Push on morphisms (covariant) opaque unfolding Values - -- action of Push on morphisms (covariant) - Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B - to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ - cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + open CommutativeMonoid using (Carrier) + open CommutativeMonoid⇒ using (arr) + + -- setoid morphism + Pushₛ : (Fin A → Fin B) → Values A ⟶ₛ Values B + Pushₛ f .to v = merge v ∘ preimage f ∘ ⁅_⁆ + Pushₛ f .cong x≗y i = merge-cong (preimage f ⁅ i ⁆) x≗y + + opaque + + unfolding Pushₛ _⊕_ + + Push-⊕ + : (f : Fin A → Fin B) + → (xs ys : ∣ Values A ∣) + → Pushₛ f ⟨$⟩ (xs ⊕ ys) + ≋ (Pushₛ f ⟨$⟩ xs) ⊕ (Pushₛ f ⟨$⟩ ys) + Push-⊕ f xs ys i = merge-⊕ xs ys (preimage f ⁅ i ⁆) + + Push-<ε> + : (f : Fin A → Fin B) + → Pushₛ f ⟨$⟩ <ε> ≋ <ε> + Push-<ε> f i = merge-<ε> (preimage f ⁅ i ⁆) + + opaque + + unfolding Push-⊕ ≋-isEquiv Valuesₘ + + -- monoid morphism + Pushₘ : (Fin A → Fin B) → CommutativeMonoid⇒ (Valuesₘ A) (Valuesₘ B) + Pushₘ f = record + { monoid⇒ = record + { arr = Pushₛ f + ; preserves-μ = Push-⊕ f _ _ + ; preserves-η = Push-<ε> f + } + } -- Push respects identity - Push-identity : Push₁ id ≈ Id (Values A) - Push-identity {_} {v} = merge-⁅⁆ v + Push-identity + : (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ A))) + → arr (Pushₘ id) ≈ Id (Carrier (Push₀ A)) + Push-identity {_} {v} i = merge-⁅⁆ v i + + opaque + + unfolding Pushₘ push -- Push respects composition Push-homomorphism : {f : Fin A → Fin B} {g : Fin B → Fin C} - → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f - Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ C))) + → arr (Pushₘ (g ∘ f)) ≈ arr (Pushₘ g) ∙ arr (Pushₘ f) + Push-homomorphism {f = f} {g} {v} = merge-push f g v -- Push respects equality Push-resp-≈ : {f g : Fin A → Fin B} → f ≗ g - → Push₁ f ≈ Push₁ g + → (open Setoid (Carrier (Push₀ A) ⇒ₛ Carrier (Push₀ B))) + → arr (Pushₘ f) ≈ arr (Pushₘ g) Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ -opaque - - unfolding Push₁ - - Push-defs : ⊤ - Push-defs = tt - -- the Push functor -Push : Functor Nat (Setoids 0ℓ 0ℓ) -F₀ Push = Values -F₁ Push = Push₁ -identity Push = Push-identity -homomorphism Push = Push-homomorphism -F-resp-≈ Push = Push-resp-≈ +Push : Functor Nat CMonoids +Push .F₀ = Push₀ +Push .F₁ = Pushₘ +Push .identity = Push-identity +Push .homomorphism = Push-homomorphism +Push .F-resp-≈ = Push-resp-≈ module Push = Functor Push |