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

open import Algebra using (CommutativeSemiring)
open import Level using (Level; _⊔_)

module Data.Matrix.FreeSemimodule {c ℓ : Level} (R : CommutativeSemiring c ℓ) where

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 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.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-∘; 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; ⟨ε⟩; ⊕-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

  unfolding _[_] _⟨_⟩

  -[-⟨-⟩] : {A B : ℕ} (M : Matrix A B) (r : Carrier) (V : Vector A) → M [ r ⟨ V ⟩ ] ≊ r ⟨ M [ V ] ⟩
  -[-⟨-⟩] {A} M r V = begin
      map (λ x → x ∙ r ⟨ V ⟩) M ≈⟨ PW.map⁺ lemma {xs = M} ≋.refl ⟩
      map (λ x → r * x ∙ V) M   ≡⟨ map-∘ (r *_) (_∙ V) M ⟩
      map (r *_) (map (_∙ V) M) ∎
    where
      lemma : {X Y : Vector A} → X ≊ Y → X ∙ r ⟨ V ⟩ ≈ r * Y ∙ V
      lemma {X} {Y} X≊Y = begin
          X ∙ r ⟨ V ⟩ ≈⟨ ∙-cong ≊.refl (⟨-⟩-comm r V) ⟩
          X ∙ ⟨ V ⟩ r ≈⟨ *-∙ʳ X V r ⟨
          X ∙ V * r   ≈⟨ *-comm (X ∙ V) r ⟩
          r * X ∙ V   ≈⟨ *-congˡ (∙-cong X≊Y ≊.refl) ⟩
          r * Y ∙ V   ∎
        where
          open ≈-Reasoning R.setoid
      open ≈-Reasoning (Vectorₛ _)

  -[⟨-⟩-] : {A B : ℕ} (M : Matrix A B) (r : Carrier) (V : Vector A) → M [ ⟨ V ⟩ r ] ≊ ⟨ M [ V ] ⟩ r
  -[⟨-⟩-] {A} {B} M r V = begin
      map (λ x → x ∙ ⟨ V ⟩ r) M ≈⟨ PW.map⁺ (λ {W} ≊W → trans (*-∙ʳ W V r) (∙-cong ≊W ≊.refl)) {xs = M} ≋.refl ⟨
      map (λ x → x ∙ V * r) M   ≡⟨ map-∘ (_* r) (_∙ V) M ⟩
      map (_* r) (map (_∙ V) M) ∎
    where
      open ≈-Reasoning (Vectorₛ _)

F₁  : {A B : ℕ}
    → Matrix A B
    → SemimoduleHomomorphism (Vector-Semimodule A) (Vector-Semimodule B)
F₁ M = record
    { ⟦_⟧ = M [_]
    ; isSemimoduleHomomorphism = record
        { isBisemimoduleHomomorphism = record
            { +ᴹ-isMonoidHomomorphism = record
                { isMagmaHomomorphism = record
                    { isRelHomomorphism = record
                        { cong = -[-]-cong M
                        }
                    ; homo = -[⊕] M
                    }
                ; ε-homo = -[⟨0⟩] M
                }
            ; *ₗ-homo = -[-⟨-⟩] M
            ; *ᵣ-homo = -[⟨-⟩-] M
            }
        }
    }

Free : Functor Mat Semimodules
Free = record
    { F₀ = Vector-Semimodule
    ; F₁ = F₁
    ; identity = I[-]
    ; 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
    }