{-# OPTIONS --without-K --safe #-}

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

map : {M N : Semimodule R m ℓm}
    → SemimoduleHomomorphism M N
    → CMonoidHomomorphism m ℓm (+ᴹ-commutativeMonoid M) (+ᴹ-commutativeMonoid N)
map f = mk-⇒ record
    { ⟦_⟧ = ⟦_⟧
    ; isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism
    }
  where
    open SemimoduleHomomorphism f

+-CMonoid : Functor Semimodules (CMonoids m ℓm)
+-CMonoid = record
    { F₀ = +ᴹ-commutativeMonoid
    ; F₁ = map
    ; identity = λ {A} x → ≈ᴹ-refl A {x}
    ; homomorphism = λ {_ _ C} _ → ≈ᴹ-refl C
    ; F-resp-≈ = id
    }

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
    }