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

open import Algebra using (Semiring)
open import Category.Instance.Rigs using (RigHomomorphism)
open import Level using (Level)

module Data.Matrix.BaseChange
    {c ℓ : Level}
    (R S : Semiring c ℓ)
    (f : RigHomomorphism R S)
  where

module R = Semiring R
module S = Semiring S

import Data.Matrix.Category as MCat
import Data.Matrix.Core as MC
import Data.Matrix.Endofunctor as Endo
import Data.Matrix.Monoid as MM
import Data.Matrix.Raw as MR
import Data.Matrix.Semiadditive as MS
import Data.Matrix.Transform as MT
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
import Data.Vector.Bisemimodule as VB
import Data.Vector.Core as VC
import Data.Vector.Endofunctor.Monoid as MonEndo
import Data.Vector.Endofunctor.Setoid as VecEndo
import Data.Vector.Monoid as VM
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

open import Categories.Functor using (Functor)
open import Category.Instance.Monoids using (MonoidHomomorphism; mk-⇒)
open import Data.Matrix.Category using (Mat)
open import Data.Matrix.Semiadditive using (Mat-CC)
open import Data.Matrix.Transform using (I)
open import Data.Nat using (ℕ; _+_)
open import Data.Vec using (map; []; _∷_; zipWith; replicate)
open import Data.Vec.Properties using (map-∘; map-replicate)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
open import Data.Vector.Core S.setoid using (_≊_)
open import Data.Vector.Core using (Vector)
open import Data.Vector.Monoid using (⟨ε⟩)
open import Data.Vector.Raw using (module Relation)
open import Function using (id; Func; _⟶ₛ_; _⟨$⟩_; _∘_)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open Func
open Functor
open MC using (Matrix)
open RigHomomorphism f
open ℕ
private module Mat {A B : ℕ} = Functor (Endo.Mat A B {c} {ℓ})

open MR hiding (map; Matrix)

module MatR where
  open MC R.setoid public
  open MM R.+-monoid public
  open MT R public
  open MS R public using (Mat-CC; proj₁; proj₂)
  open MCat R using (_·_) public

module MatS where
  open MC S.setoid public
  open MM S.+-monoid public
  open MT S public
  open MS S public using (Mat-CC; isTerminal; isProduct)
  open MCat S using (_·_) public

module VecR where
  open VC R.setoid public
  open VM R.+-monoid public
  open VB R public

module VecS where
  open VC S.setoid public
  open VM S.+-monoid public
  open VB S public

change
    : {A B : ℕ}
    → Matrix R.setoid A B
    → Matrix S.setoid A B
change = to (Mat.₁ func)

resp
    : {A B : ℕ}
      {M M′ : MatR.Matrix A B}
    → M MatR.≋ M′
    → change M MatS.≋ change M′
resp = cong (Mat.₁ func)

⟨ε⟩-homo : {A : ℕ} → (map ⟦_⟧) VecR.⟨ε⟩ ≊ VecS.⟨ε⟩ {A}
⟨ε⟩-homo {A} = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism))

opaque
  unfolding I _ᵀ _∷ₕ_ Endo.mapₛ
  ident : {A : ℕ} → change (I R) MatS.≋ I S {A}
  ident {zero} = PW.[]
  ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI
    where
      map-⟨ε⟩∷ₕI : map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I) MatS.≋ VecS.⟨ε⟩ ∷ₕ MatS.I {A}
      map-⟨ε⟩∷ₕI = begin
          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I)            ≡⟨ ≡.cong (λ h → map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ h)) MatR.Iᵀ ⟨
          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I ᵀ)          ≡⟨ ≡.cong (map (map ⟦_⟧)) (∷ᵥ-ᵀ VecR.⟨ε⟩ MatR.I) ⟨
          map (map ⟦_⟧) ((VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ)        ≡⟨ Natural.α-ᵀ ⟦_⟧ (VecR.⟨ε⟩ ∷ᵥ MatR.I) ⟩
          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ          ≡⟨⟩
          (map ⟦_⟧ VecR.⟨ε⟩ ∷ᵥ map (map ⟦_⟧) MatR.I) ᵀ  ≡⟨ ∷ᵥ-ᵀ (map ⟦_⟧ VecR.⟨ε⟩) (map (map ⟦_⟧) MatR.I) ⟩
          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ (map (map ⟦_⟧) MatR.I ᵀ)  ≡⟨ ≡.cong (map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ_) (Natural.α-ᵀ ⟦_⟧ MatR.I) ⟨
          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) (MatR.I ᵀ)  ≡⟨ ≡.cong (λ h → map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) h) MatR.Iᵀ ⟩
          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) MatR.I      ≈⟨ MatS.∷ₕ-cong ⟨ε⟩-homo ident ⟩
          VecS.⟨ε⟩ ∷ₕ MatS.I                            ∎
        where
          open ≈-Reasoning (MatS.Matrixₛ (suc A) A)

opaque
  unfolding MatS.𝟎 Endo.mapₛ
  change-𝟎 : {A B : ℕ} → change MatR.𝟎 MatS.≋ MatS.𝟎 {A} {B}
  change-𝟎 {A} {B} = begin
      map (map ⟦_⟧) (replicate B VecR.⟨ε⟩)  ≡⟨ map-replicate (map ⟦_⟧) VecR.⟨ε⟩ B ⟩
      replicate B (map (to func) VecR.⟨ε⟩)  ≈⟨ Relation.R-replicate ⟨ε⟩-homo ⟩
      replicate B VecS.⟨ε⟩                  ∎
    where
      open ≈-Reasoning (MatS.Matrixₛ A B)

opaque
  unfolding VecR._∙_
  ⟦⟧-∙ : {n : ℕ} (V W : VecR.Vector n) → ⟦ V VecR.∙ W ⟧ S.≈ map ⟦_⟧ V VecS.∙ map ⟦_⟧ W
  ⟦⟧-∙ {zero} [] [] = 0#-homo
  ⟦⟧-∙ {suc n} (x ∷ V) (y ∷ W) = begin
      ⟦ x VecR.R.* y VecR.R.+ V VecR.∙ W ⟧                  ≈⟨ +-homo (x VecR.R.* y) (V VecR.∙ W) ⟩
      ⟦ x VecR.R.* y ⟧ S.+ ⟦ V VecR.∙ W ⟧                   ≈⟨ S.+-cong (*-homo x y) (⟦⟧-∙ V W) ⟩
      ⟦ x ⟧ VecS.R.* ⟦ y ⟧ S.+ (map ⟦_⟧ V VecS.∙ map ⟦_⟧ W) ∎
    where
      open ≈-Reasoning S.setoid

opaque
  unfolding VecR.⟨ε⟩
  ⟦⟧-⟨ε⟩ : {n : ℕ} → map ⟦_⟧ (VecR.⟨ε⟩ {n}) VecS.≊ VecS.⟨ε⟩
  ⟦⟧-⟨ε⟩ {n} = begin
      map ⟦_⟧ (replicate n R.0#)  ≡⟨ map-replicate ⟦_⟧ R.0# n ⟩
      replicate n ⟦ R.0# ⟧        ≈⟨ VecS.replicate-cong 0#-homo ⟩
      replicate n VecS.R.0#       ∎
    where
      open ≈-Reasoning (VecS.Vectorₛ n)

opaque
  unfolding MatR.[_]_ Endo.mapₛ
  ⟦⟧-[-]-
      : {n m : ℕ}
        (V : VecR.Vector n)
        (M : MatR.Matrix m n)
      → map ⟦_⟧ (MatR.[ V ] M) VecS.≊ MatS.[ map ⟦_⟧ V ] (change M)
  ⟦⟧-[-]- {n} {m} V M = begin
      map ⟦_⟧ (map (V VecR.∙_) (M ᵀ))                 ≡⟨ map-∘ ⟦_⟧ (V VecR.∙_) (M ᵀ) ⟨
      map (λ x → ⟦ V VecR.∙ x ⟧) (M ᵀ)                ≈⟨ PW.map⁺ (λ {x y} ≈xy → S.trans (⟦⟧-cong (VecR.∙-cong VecR.≊.refl ≈xy)) (⟦⟧-∙ V y)) MatR.≋.refl ⟩
      map (λ x → map ⟦_⟧ V VecS.∙ map ⟦_⟧ x) (M ᵀ)    ≡⟨ map-∘ ((map ⟦_⟧ V) VecS.∙_) (map ⟦_⟧) (M ᵀ) ⟩
      map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) (M ᵀ)) ≡⟨ ≡.cong ( map ((map ⟦_⟧ V) VecS.∙_)) (Natural.α-ᵀ ⟦_⟧ M) ⟩
      map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) M ᵀ)   ∎
    where
      open ≈-Reasoning (VecS.Vectorₛ m)

opaque
  unfolding Endo.mapₛ MatR.[_]_
  homo
      : {X Y Z : ℕ}
        {M : MatR.Matrix X Y}
        {N : MatR.Matrix Y Z}
      → change (N MatR.· M) MatS.≋ change N MatS.· change M
  homo {X} {Y} {Z} {M} {[]} = PW.[]
  homo {X} {Y} {suc Z} {M} {N₀ ∷ N} = ⟦⟧-[-]- N₀ M PW.∷ homo {X} {Y} {Z} {M} {N}

ChangeBase : Functor (Mat R) (Mat S)
ChangeBase = record
    { F₀ = id
    ; F₁ = change
    ; identity = ident
    ; homomorphism = homo
    ; F-resp-≈ = resp
    }

open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)

open import Categories.Object.Product using (IsProduct)

open import Categories.Category using (Category)
module _ {o ℓ e : Level} {𝒞 : Category o ℓ e} where

  open Category 𝒞
  open HomReasoning
  open Equiv

  IsProduct-cong
      : {P A B : Obj} {f f′ : P ⇒ A} {g g′ : P ⇒ B}
      → f ≈ f′
      → g ≈ g′
      → IsProduct 𝒞 f g
      → IsProduct 𝒞 f′ g′
  IsProduct-cong ≈f ≈g isProduct = let open IsProduct 𝒞 isProduct in record
      { ⟨_,_⟩ = ⟨_,_⟩
      ; project₁ = sym ≈f ⟩∘⟨refl ○ project₁
      ; project₂ = sym ≈g ⟩∘⟨refl ○ project₂
      ; unique = λ eq₁ eq₂ → unique (≈f ⟩∘⟨refl ○ eq₁) (≈g ⟩∘⟨refl ○ eq₂)
      }

opaque
  unfolding Endo.mapₛ
  change-∥ : {A B C : ℕ} {M : Matrix R.setoid A C} {N : Matrix R.setoid B C} → change (M ∥ N) ≡ change M ∥ change N
  change-∥ {M = M} {N} = Natural.α-∥ ⟦_⟧ M N

ChangeBase-resp-×
    : {A B : ℕ}
    → IsProduct (Mat S) (change (MatR.I {A} ∥ MatR.𝟎)) (change (MatR.𝟎 ∥ MatR.I {B}))
ChangeBase-resp-× {A} {B} = IsProduct-cong eq₁ eq₂ MatS.isProduct
  where
    eq₁ : MatS.I ∥ MatS.𝟎 MatS.≋ change (MatR.I ∥ MatR.𝟎)
    eq₁ = begin
        MatS.I ∥ MatS.𝟎               ≈⟨ MatS.∥-cong ident change-𝟎 ⟨
        change MatR.I ∥ change MatR.𝟎 ≡⟨ change-∥ ⟨
        change (MatR.I ∥ MatR.𝟎)      ∎
      where
        open ≈-Reasoning (MatS.Matrixₛ (A + B) A)
    eq₂ : MatS.𝟎 ∥ MatS.I MatS.≋ change (MatR.𝟎 ∥ MatR.I)
    eq₂ = begin
        MatS.𝟎 ∥ MatS.I               ≈⟨ MatS.∥-cong change-𝟎 ident ⟨
        change MatR.𝟎 ∥ change MatR.I ≡⟨ change-∥ ⟨
        change (MatR.𝟎 ∥ MatR.I)      ∎
      where
        open ≈-Reasoning (MatS.Matrixₛ (A + B) B)

ChangeBase-IsCF : IsCartesianF (Mat-CC R) (Mat-CC S) ChangeBase
ChangeBase-IsCF = record
    { F-resp-⊤ = MatS.isTerminal
    ; F-resp-× = ChangeBase-resp-×
    }

ChangeBase-CF : CartesianF (Mat-CC R) (Mat-CC S)
ChangeBase-CF = record
    { F = ChangeBase
    ; isCartesian = ChangeBase-IsCF
    }