From 61549e3d703bdc5a017833a01febb9c46d95ec17 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 7 Jul 2026 13:09:11 -0700 Subject: Update matrices and vectors --- Data/Vector/Endofunctor/Monoid.agda | 106 ++++++++++++++++++++++++++++++++++++ Data/Vector/Endofunctor/Setoid.agda | 81 +++++++++++++++++++++++++++ 2 files changed, 187 insertions(+) create mode 100644 Data/Vector/Endofunctor/Monoid.agda create mode 100644 Data/Vector/Endofunctor/Setoid.agda (limited to 'Data/Vector/Endofunctor') diff --git a/Data/Vector/Endofunctor/Monoid.agda b/Data/Vector/Endofunctor/Monoid.agda new file mode 100644 index 0000000..217c754 --- /dev/null +++ b/Data/Vector/Endofunctor/Monoid.agda @@ -0,0 +1,106 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in monoids sending A to Vectorₘ A n for a fixed n +module Data.Vector.Endofunctor.Monoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra using (Monoid) +open import Categories.Category using (Category; _[_∘_]; _[_≈_]) +open import Categories.Functor using (Functor) +open import Category.Instance.Monoids using (Monoids; MonoidHomomorphism; mk-⇒) +open import Data.Monoid using (toMonoid) +open import Data.Vec.Properties using (map-replicate) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊; replicate-cong) +open import Data.Vector.Endofunctor.Setoid as Endo using (mapₛ; zipWith-cong) +open import Data.Vector.Monoid as Mon using (Vectorₘ; ⟨ε⟩) renaming (_⊕_ to _[_⊕_]) +open import Data.Vector.Vec using (map-zipWith; zipWith-map-map) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) + +open Func +open MonoidHomomorphism + +private module _ {M N : Monoid c ℓ} (f : MonoidHomomorphism c ℓ M N) where + + private + module M = Monoid M + module N = Monoid N + + open Core N.setoid using (_≊_) + open ≈-Reasoning (Vectorₛ N.setoid n) + + opaque + unfolding _[_⊕_] + map-⊕ + : (W V : Vector M.setoid n) + → mapₛ n (func f) ⟨$⟩ (M [ W ⊕ V ]) + ≊ N [ mapₛ n (func f) ⟨$⟩ W ⊕ mapₛ n (func f) ⟨$⟩ V ] + map-⊕ W V = begin + Vec.map ⟦ f ⟧ (Vec.zipWith M._∙_ W V) ≡⟨ map-zipWith ⟦ f ⟧ M._∙_ W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ (x M.∙ y)) W V ≈⟨ zipWith-cong n N.setoid (homo f) W V ⟩ + Vec.zipWith (λ x y → ⟦ f ⟧ x N.∙ ⟦ f ⟧ y) W V ≡⟨ zipWith-map-map ⟦ f ⟧ ⟦ f ⟧ N._∙_ W V ⟩ + Vec.zipWith N._∙_ (Vec.map ⟦ f ⟧ W) (Vec.map ⟦ f ⟧ V) ∎ + + opaque + unfolding ⟨ε⟩ + map-⟨ε⟩ : mapₛ n (func f) ⟨$⟩ (Mon.⟨ε⟩ M) ≊ Mon.⟨ε⟩ N + map-⟨ε⟩ = begin + Vec.map (to (func f)) (Vec.replicate n M.ε) ≡⟨ map-replicate (to (func f)) M.ε n ⟩ + Vec.replicate n (func f ⟨$⟩ M.ε) ≈⟨ replicate-cong N.setoid (ε-homo f) ⟩ + Vec.replicate n N.ε ∎ + +mapₘ : {M N : Monoid c ℓ} → MonoidHomomorphism c ℓ M N → MonoidHomomorphism c (c ⊔ ℓ) (Vectorₘ M n) (Vectorₘ N n) +mapₘ {M} {N} f = mk-⇒ record + { ⟦_⟧ = to (mapₛ n (func f)) + ; isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = map⁺ (⟦⟧-cong f) + } + ; homo = map-⊕ f + } + ; ε-homo = map-⟨ε⟩ f + } + } + +open Category using (id) + +abstract + + identity + : {A : Monoid c ℓ} + → Monoids c (c ⊔ ℓ) [ mapₘ (id (Monoids c ℓ) {A}) ≈ id (Monoids c (c ⊔ ℓ)) ] + identity {A} V = Endo.identity n {c} {ℓ} {Monoid.setoid A} + + homomorphism + : {X Y Z : Monoid c ℓ} + {f : MonoidHomomorphism c ℓ X Y} + {g : MonoidHomomorphism c ℓ Y Z} + → Monoids c (c ⊔ ℓ) [ mapₘ (Monoids c ℓ [ g ∘ f ]) ≈ Monoids c (c ⊔ ℓ) [ mapₘ g ∘ mapₘ f ] ] + homomorphism {X} {Y} {Z} {f} {g} V = Endo.homomorphism n {c} {ℓ} {setoid X} {setoid Y} {setoid Z} {func f} {func g} {V} + where + open Monoid using (setoid) + + F-resp-≈ + : {A B : Monoid c ℓ} + {f g : MonoidHomomorphism c ℓ A B} + → Monoids c ℓ [ f ≈ g ] + → Monoids c (c ⊔ ℓ) [ mapₘ f ≈ mapₘ g ] + F-resp-≈ {A} {B} {f} {g} f≈g V = Endo.F-resp-≈ n {c} {ℓ} {setoid A} {setoid B} {func f} {func g} (λ {x} → f≈g x) + where + open Monoid using (setoid) + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Monoids c ℓ) (Monoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ M → Vectorₘ M n + ; F₁ = mapₘ + ; identity = λ {M} → identity {M} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } diff --git a/Data/Vector/Endofunctor/Setoid.agda b/Data/Vector/Endofunctor/Setoid.agda new file mode 100644 index 0000000..09f8f69 --- /dev/null +++ b/Data/Vector/Endofunctor/Setoid.agda @@ -0,0 +1,81 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +-- The endofunctor in setoids sending A to Vector A n for a fixed n +module Data.Vector.Endofunctor.Setoid (n : ℕ) {c ℓ : Level} where + +import Data.Vec as Vec + +open import Categories.Category using (_[_≈_]) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Setoid using (∣_∣) +open import Data.Vec.Properties using (map-id; map-∘) +open import Data.Vec.Relation.Binary.Equality.Setoid using () renaming (_≋_ to _[_≋_]) +open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (map⁺; Pointwise) +open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊) +open import Data.Vector.Raw using (R-zipWith) +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 Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open Func +open ℕ +open Vec.Vec +open Pointwise + +mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n +mapₛ f .to = Vec.map (to f) +mapₛ f .cong = map⁺ (cong f) + +abstract + + identity + : {A : Setoid c ℓ} + {V : Vector A n} + (open Core A using (_≊_)) + → mapₛ (Id A) ⟨$⟩ V ≊ V + identity {A} {V} = ≊.reflexive A (map-id V) + + homomorphism + : {X Y Z : Setoid c ℓ} + {f : X ⟶ₛ Y} + {g : Y ⟶ₛ Z} + {V : Vector X n} + (open Core Z using (_≊_)) + → mapₛ (compose f g) ⟨$⟩ V ≊ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ V) + homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V) + + F-resp-≈ + : {A B : Setoid c ℓ} + {f g : A ⟶ₛ B} + → Setoids c ℓ [ f ≈ g ] + → Setoids c (c ⊔ ℓ) [ mapₛ f ≈ mapₛ g ] + F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A) + where + module B = Setoid B + +-- only a true endofunctor when c ≤ ℓ +Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) +Vec = record + { F₀ = λ A → Vectorₛ A n + ; F₁ = mapₛ + ; identity = λ {A} → identity {A} + ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g} + ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g} + } + +zipWith-cong + : {A B : Set c} + (C : Setoid c ℓ) + (let module C = Setoid C) + {f g : A → B → ∣ C ∣} + → (∀ x y → f x y C.≈ g x y) + → (xs : Vec.Vec A n) + (ys : Vec.Vec B n) + → C [ Vec.zipWith f xs ys ≋ Vec.zipWith g xs ys ] +zipWith-cong C f≈g xs ys = R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≈g _ _}) (PW.refl ≡.refl) (PW.refl ≡.refl) -- cgit v1.2.3