Show semimodules forgetful functor is cartesian

1 files changed, 81 insertions, 1 deletions

diff --git a/Functor/Forgetful/Instance/Semimodule.agda b/Functor/Forgetful/Instance/Semimodule.agda
index 59f4b61..929602e 100644
--- a/Functor/Forgetful/Instance/Semimodule.agda
+++ b/Functor/Forgetful/Instance/Semimodule.agda
@@ -1,14 +1,22 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Algebra using (CommutativeSemiring)
+open import Algebra using (CommutativeSemiring; CommutativeMonoid)
 open import Level using (Level)
 
 module Functor.Forgetful.Instance.Semimodule {c ℓ m ℓm : Level} (R : CommutativeSemiring c ℓ) where
 
+import Algebra.Module.Construct.DirectProduct as DirectProduct
+
 open import Algebra.Module using (Semimodule)
+open import Categories.Category using (Category)
 open import Categories.Functor using (Functor)
+open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)
+open import Category.Cartesian.Instance.CMonoids using (CMonoids-CC)
+open import Category.Cartesian.Instance.Semimodules {c} {ℓ} {m} {ℓm} R using (Semimodules-CC; π₁; π₂)
 open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism; mk-⇒)
 open import Category.Instance.Semimodules {c} {ℓ} {m} {ℓm} R using (Semimodules; SemimoduleHomomorphism)
+open import Data.Product using (_,_)
+open import Data.Unit.Polymorphic using (tt)
 open import Function using (id)
 
 open Semimodule
@@ -33,3 +41,75 @@ map f = mk-⇒ record
     }
 
 module +-CMonoid = Functor +-CMonoid
+
+module _ (A B : Semimodule R m ℓm) where
+
+  open CMonoidHomomorphism using (⟦_⟧; ⟦⟧-cong; ε-homo; homo)
+  open Category (CMonoids m ℓm) using (_∘_; _≈_)
+
+  private
+    module A = Semimodule A
+    module B = Semimodule B
+
+  module _
+    {C : CommutativeMonoid m ℓm}
+    {f : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid A)}
+    {g : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid B)} where
+
+    <> : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid (DirectProduct.semimodule A B))
+    <> = mk-⇒ record
+        { ⟦_⟧ = λ x → ⟦ f ⟧ x , ⟦ g ⟧ x
+        ; isMonoidHomomorphism = record
+            { isMagmaHomomorphism = record
+                { isRelHomomorphism = record
+                    { cong = λ x → ⟦⟧-cong f x , ⟦⟧-cong g x
+                    }
+                ; homo = λ x y → homo f x y , homo g x y
+                }
+            ; ε-homo = ε-homo f , ε-homo g
+            }
+        }
+
+    project₁ : map (π₁ A B) ∘ <> ≈ f
+    project₁ _ = ≈ᴹ-refl A
+
+    project₂ : map (π₂ A B) ∘ <> ≈ g
+    project₂ _ = ≈ᴹ-refl B
+
+    unique
+        : {h : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid (DirectProduct.semimodule A B))}
+        → map (π₁ A B) ∘ h ≈ f
+        → map (π₂ A B) ∘ h ≈ g
+        → <> ≈ h
+    unique eq₁ eq₂ x = ≈ᴹ-sym A (eq₁ x) , ≈ᴹ-sym B (eq₂ x)
+
++-CMonoid-IsCF : IsCartesianF Semimodules-CC CMonoids-CC +-CMonoid
++-CMonoid-IsCF = record
+    { F-resp-⊤ = record
+        { ! = mk-⇒ record
+            { ⟦_⟧ = λ _ → tt
+            ; isMonoidHomomorphism = record
+                { isMagmaHomomorphism = record
+                    { isRelHomomorphism = record
+                        { cong = λ _ → tt
+                        }
+                    ; homo = λ _ _ → tt
+                    }
+                ; ε-homo = tt
+                }
+            }
+        ; !-unique = λ _ _ → tt
+        }
+    ; F-resp-× = λ {A B} → record
+        { ⟨_,_⟩ = λ {C} f g → <> A B {C} {f} {g}
+        ; project₁ = λ {C f g} → project₁ A B {C} {f} {g}
+        ; project₂ = λ {C f g} → project₂ A B {C} {f} {g}
+        ; unique = λ {C h f g} → unique A B {C} {f} {g} {h}
+        }
+    }
+
++-CMonoid-CF : CartesianF Semimodules-CC CMonoids-CC
++-CMonoid-CF = record
+    { F = +-CMonoid
+    ; isCartesian = +-CMonoid-IsCF
+    }