Show free semimodule functor is cartesian

1 files changed, 188 insertions, 5 deletions

diff --git a/Data/Matrix/FreeSemimodule.agda b/Data/Matrix/FreeSemimodule.agda
index 77f2fe3..210d2e4 100644
--- a/Data/Matrix/FreeSemimodule.agda
+++ b/Data/Matrix/FreeSemimodule.agda
@@ -10,20 +10,33 @@ module R = CommutativeSemiring R
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
+open import Algebra.Module using (Semimodule)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Functor using (Functor)
-open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism)
+open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)
+open import Categories.Object.Product using (IsProduct)
+open import Categories.Object.Terminal using (IsTerminal)
+open import Category.Cartesian.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules-CC)
+open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism) renaming (_≈_ to _≈-SM_)
 open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-[])
 open import Data.Matrix.Core R.setoid using (Matrix; module ≋)
-open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕])
-open import Data.Nat using (ℕ)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎)
+open import Data.Matrix.Raw using (_∥_; _≑_)
+open import Data.Matrix.Semiadditive R.semiring using (Mat-CC)
+open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕]; ∥-[++]; 𝟎-[-]; ≑--[-]; I-∥-≑)
+open import Data.Nat as Nat using (ℕ)
+open import Data.Vec using ([]; _++_)
 open import Data.Vec using (map)
-open import Data.Vec.Properties using (map-∘)
+open import Data.Vec.Properties using (map-∘; map-++; zipWith-++)
 open import Data.Vector.Bisemimodule R.semiring using (_⟨_⟩; ⟨_⟩_; _∙_; *-∙ˡ; *-∙ʳ; ∙-cong)
 open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; _≊_; module ≊)
-open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⟨ε⟩)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⟨ε⟩; ⊕-identityˡ; ⊕-identityʳ)
 open import Data.Vector.Semimodule R using (Vector-Semimodule; ⟨-⟩-comm)
+open import Data.Vector.Vec using (replicate-++)
+open import Relation.Binary using (Setoid)
 
 open R
+open SemimoduleHomomorphism using (⟦_⟧; ⟦⟧-cong)
 
 opaque
 
@@ -84,3 +97,173 @@ Free = record
     ; homomorphism = λ {f = M} {N} V → ·-[] M N V
     ; F-resp-≈ = -[-]-cong₁
     }
+
+
+module Free-resp-⊤ where
+
+  opaque
+    unfolding _⊕_ ⟨ε⟩ _⟨_⟩
+    ! : {A : Semimodule R c (c ⊔ ℓ)} → SemimoduleHomomorphism A (Vector-Semimodule 0)
+    ! {A} = record
+        { ⟦_⟧ = λ _ → []
+        ; isSemimoduleHomomorphism = record
+            { isBisemimoduleHomomorphism = record
+                { +ᴹ-isMonoidHomomorphism = record
+                    { isMagmaHomomorphism = record
+                        { isRelHomomorphism = record
+                            { cong = λ _ → PW.[]
+                            }
+                        ; homo = λ _ _ → PW.[]
+                        }
+                    ; ε-homo = PW.[]
+                    }
+                ; *ₗ-homo = λ _ _ → PW.[]
+                ; *ᵣ-homo = λ _ _ → PW.[]
+                }
+            }
+        }
+
+    !-unique
+        : {A : Semimodule R c (c ⊔ ℓ)}
+          (f : SemimoduleHomomorphism A (Vector-Semimodule 0))
+        → ! ≈-SM f
+    !-unique f x with [] ← ⟦ f ⟧ x = PW.[]
+
+Free-resp-⊤ : IsTerminal Semimodules (Vector-Semimodule Mat-CC.⊤)
+Free-resp-⊤ = record { Free-resp-⊤ }
+
+⟨_,_⟩
+    : {A B : ℕ}
+      {X : Semimodule R c (c ⊔ ℓ)}
+    → SemimoduleHomomorphism X (Vector-Semimodule A)
+    → SemimoduleHomomorphism X (Vector-Semimodule B)
+    → SemimoduleHomomorphism X (Vector-Semimodule (A Nat.+ B))
+⟨_,_⟩ {A} {B} {X} f g = record
+    { ⟦_⟧ = λ x → ⟦ f ⟧ x ++ ⟦ g ⟧ x
+    ; isSemimoduleHomomorphism = record
+        { isBisemimoduleHomomorphism = record
+            { +ᴹ-isMonoidHomomorphism = record
+                { isMagmaHomomorphism = record
+                    { isRelHomomorphism = record
+                        { cong = λ ≈x → PW.++⁺ (⟦⟧-cong f ≈x) (⟦⟧-cong g ≈x)
+                        }
+                    ; homo = homo
+                    }
+                ; ε-homo = ε-homo
+                }
+            ; *ₗ-homo = *ₗ-homo
+            ; *ᵣ-homo = *ᵣ-homo
+            }
+        }
+    }
+  where
+    open ≈-Reasoning (PW.setoid setoid (A Nat.+ B))
+    module f = SemimoduleHomomorphism f
+    module g = SemimoduleHomomorphism g
+    open Semimodule X
+    opaque
+      unfolding ⟨ε⟩
+      ε-homo : PW.Pointwise {c} {c} {ℓ} {Carrier} {Carrier} _≈_ {A Nat.+ B} {A Nat.+ B} (⟦ f ⟧ 0ᴹ ++ ⟦ g ⟧ 0ᴹ) ⟨ε⟩
+      ε-homo = begin
+        ⟦ f ⟧ 0ᴹ ++ ⟦ g ⟧ 0ᴹ  ≈⟨ PW.++⁺ f.0ᴹ-homo g.0ᴹ-homo ⟩
+        ⟨ε⟩ {A} ++ ⟨ε⟩ {B}    ≡⟨ replicate-++ A B 0# ⟩
+        ⟨ε⟩                   ∎
+    opaque
+      unfolding _⊕_
+      homo : (x y : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ x +ᴹ y ⟧ ++ g.⟦ x +ᴹ y ⟧) ((f.⟦ x ⟧ ++ g.⟦ x ⟧) ⊕ (f.⟦ y ⟧ ++ g.⟦ y ⟧))
+      homo x y = begin
+          f.⟦ x +ᴹ y ⟧ ++ g.⟦ x +ᴹ y ⟧                ≈⟨ PW.++⁺ (f.+ᴹ-homo x y) (g.+ᴹ-homo x y) ⟩
+          (f.⟦ x ⟧ ⊕ f.⟦ y ⟧) ++ (g.⟦ x ⟧ ⊕ g.⟦ y ⟧)  ≡⟨ zipWith-++ _+_ f.⟦ x ⟧ g.⟦ x ⟧ f.⟦ y ⟧ g.⟦ y ⟧ ⟨
+          (f.⟦ x ⟧ ++ g.⟦ x ⟧) ⊕ (f.⟦ y ⟧ ++ g.⟦ y ⟧) ∎
+    opaque
+      unfolding _⟨_⟩
+      *ₗ-homo : (r : Carrier) (x : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ r *ₗ x ⟧ ++ g.⟦ r *ₗ x ⟧) (r ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩)
+      *ₗ-homo r x = begin
+          f.⟦ r *ₗ x ⟧ ++ g.⟦ r *ₗ x ⟧    ≈⟨ PW.++⁺ (f.*ₗ-homo r x) (g.*ₗ-homo r x) ⟩
+          r ⟨ f.⟦ x ⟧ ⟩ ++ r ⟨ g.⟦ x ⟧ ⟩  ≡⟨ map-++ (r *_) f.⟦ x ⟧ g.⟦ x ⟧ ⟨
+          r ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩        ∎
+    opaque
+      unfolding ⟨_⟩_
+      *ᵣ-homo : (r : Carrier) (x : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ x *ᵣ r ⟧ ++ g.⟦ x *ᵣ r ⟧) (⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩ r)
+      *ᵣ-homo r x = begin
+          f.⟦ x *ᵣ r ⟧ ++ g.⟦ x *ᵣ r ⟧    ≈⟨ PW.++⁺ (f.*ᵣ-homo r x) (g.*ᵣ-homo r x) ⟩
+          ⟨ f.⟦ x ⟧ ⟩ r ++ ⟨ g.⟦ x ⟧ ⟩ r  ≡⟨ map-++ (_* r) f.⟦ x ⟧ g.⟦ x ⟧ ⟨
+          ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩ r        ∎
+
+module Project
+    {A B : ℕ}
+    {X : Semimodule R c (c ⊔ ℓ)}
+    {f : SemimoduleHomomorphism X (Vector-Semimodule A)}
+    {g : SemimoduleHomomorphism X (Vector-Semimodule B)}
+  where
+
+  module f = SemimoduleHomomorphism f
+  module g = SemimoduleHomomorphism g
+  open Semimodule X
+
+  project₁ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((I {A} ∥ 𝟎 ) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]) f.⟦ x ⟧
+  project₁ x = begin
+      (I ∥ 𝟎) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]  ≈⟨ ∥-[++] f.⟦ x ⟧ g.⟦ x ⟧ I 𝟎 ⟩
+      I [ f.⟦ x ⟧ ] ⊕ 𝟎 [ g.⟦ x ⟧ ]   ≈⟨ ⊕-cong (I[-] f.⟦ x ⟧) (𝟎-[-] g.⟦ x ⟧) ⟩
+      f.⟦ x ⟧ ⊕ ⟨ε⟩                   ≈⟨ ⊕-identityʳ f.⟦ x ⟧ ⟩
+      f.⟦ x ⟧                         ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid A)
+
+  project₂ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((𝟎 ∥ I {B} ) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]) g.⟦ x ⟧
+  project₂ x = begin
+      (𝟎 ∥ I) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]  ≈⟨ ∥-[++] f.⟦ x ⟧ g.⟦ x ⟧ 𝟎 I ⟩
+      𝟎 [ f.⟦ x ⟧ ] ⊕ I [ g.⟦ x ⟧ ]   ≈⟨ ⊕-cong (𝟎-[-] f.⟦ x ⟧) (I[-] g.⟦ x ⟧) ⟩
+      ⟨ε⟩ ⊕ g.⟦ x ⟧                   ≈⟨ ⊕-identityˡ g.⟦ x ⟧ ⟩
+      g.⟦ x ⟧                         ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid B)
+
+module Unique
+    {A B : ℕ}
+    {X : Semimodule R c (c ⊔ ℓ)}
+    {f : SemimoduleHomomorphism X (Vector-Semimodule A)}
+    {g : SemimoduleHomomorphism X (Vector-Semimodule B)}
+    {h : SemimoduleHomomorphism X (Vector-Semimodule (A Nat.+ B))}
+  where
+
+  open Semimodule X
+
+  module f = SemimoduleHomomorphism f
+  module g = SemimoduleHomomorphism g
+  module h = SemimoduleHomomorphism h
+
+  unique
+      : (eq₁ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((I {A} ∥ 𝟎) [ h.⟦ x ⟧ ]) (f.⟦ x ⟧))
+      → (eq₂ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((𝟎 ∥ I {B}) [ h.⟦ x ⟧ ]) (g.⟦ x ⟧))
+      → (x : Carrierᴹ)
+      → PW.Pointwise _≈_ (f.⟦ x ⟧ ++ g.⟦ x ⟧) h.⟦ x ⟧
+  unique eq₁ eq₂ x = begin
+      f.⟦ x ⟧ ++ g.⟦ x ⟧                                  ≈⟨ PW.++⁺ (eq₁ x) (eq₂ x) ⟨
+      ((I {A} ∥ 𝟎) [ h.⟦ x ⟧ ]) ++ ((𝟎 ∥ I) [ h.⟦ x ⟧ ])  ≡⟨ ≑--[-] h.⟦ x ⟧ (I ∥ 𝟎) (𝟎 ∥ I) ⟨
+      ((I {A} ∥ 𝟎) ≑ (𝟎 ∥ I)) [ h.⟦ x ⟧ ]                 ≡⟨ ≡.cong (_[ h.⟦ x ⟧ ]) I-∥-≑ ⟩
+      I [ h.⟦ x ⟧ ]                                       ≈⟨ I[-] h.⟦ x ⟧ ⟩
+      h.⟦ x ⟧                                             ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid (A Nat.+ B))
+      open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+Free-resp-× : {A B : ℕ} → IsProduct Semimodules (F₁ (Mat-CC.π₁ {A} {B})) (F₁ (Mat-CC.π₂ {A} {B}))
+Free-resp-× {A} {B} = record
+    { ⟨_,_⟩ = ⟨_,_⟩
+    ; project₁ = λ {X f g} → Project.project₁ {A} {B} {X} {f} {g}
+    ; project₂ = λ {X f g} → Project.project₂ {A} {B} {X} {f} {g}
+    ; unique = λ {X h f g} eq₁ eq₂ x → Unique.unique {A} {B} {X} {f} {g} {h} eq₁ eq₂ x
+    }
+
+Free-IsCartesianF : IsCartesianF Mat-CC Semimodules-CC Free
+Free-IsCartesianF = record
+    { F-resp-⊤ = Free-resp-⊤
+    ; F-resp-× = Free-resp-×
+    }
+
+Free-IsCC : CartesianF Mat-CC Semimodules-CC
+Free-IsCC = record
+    { F = Free
+    ; isCartesian = Free-IsCartesianF
+    }