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

open import Level using (Level; _⊔_)
open import Relation.Binary using (Rel; REL)

module Data.Matrix.Raw where

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Vec as Vec using (Vec; zipWith; head; tail; replicate; concat; foldr)
open import Data.Vec using (_++_)
open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-const; map-replicate; zipWith-map₂; zipWith-++; zipWith-replicate)
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW-Vec using (Pointwise; map⁺)
open import Data.Vector.Raw as Vector using (R-zipWith)
open import Data.Vector.Vec using (zipWith-map; replicate-++; map-zipWith; zipWith-map-map; zipWith-cong)
open import Function using (id; _∘_; const)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)

open ℕ
open Vec.Vec

private
  variable
    n m p q : ℕ
    a ℓ ℓ₁ ℓ₂ : Level
    A B C D E F : Set a

open ≡-Reasoning

opaque

  -- Matrices
  Matrix : Set a → Rel ℕ a
  Matrix A n m = Vec (Vec A n) m

  -- Pointwise relation on matrices
  PW : {a b : Level} {A : Set a} {B : Set b} (R : REL A B ℓ) → REL (Matrix A n m) (Matrix B n m) (a ⊔ b ⊔ ℓ)
  PW R = Pointwise (Pointwise R)

  -- Apply a function to every element
  map : (A → B) → Matrix A n m → Matrix B n m
  map f = Vec.map (Vec.map f)

  -- Lift a square in the double category of sets and relations to matrices
  map₂
      : {R : REL A B ℓ}
        {S : REL C D ℓ}
        {f : A → C}
        {g : B → D}
      → (∀ {x y} → R x y → S (f x) (g y))
      → {M₁ : Matrix A m n}
        {M₂ : Matrix B m n}
      → PW R M₁ M₂
      → PW S (map f M₁) (map g M₂)
  map₂ R⇒S = map⁺ (map⁺ R⇒S)

  -- Juxtapose matrices horizontally
  _∥_ : Matrix A n p → Matrix A m p → Matrix A (n + m) p
  _∥_ M N = zipWith _++_ M N

  infixr 7 _∥_

  -- Juxtapose matrices verically
  _≑_ : Matrix A n m → Matrix A n p → Matrix A n (m + p)
  _≑_ = _++_

  infixr 6 _≑_

  -- Append a column on the left
  _∷ₕ_ : Vec A m → Matrix A n m → Matrix A (suc n) m
  _∷ₕ_ = zipWith _∷_

  infixr 5 _∷ₕ_

  -- Append a row to the top
  _∷ᵥ_ : Vec A n → Matrix A n m → Matrix A n (suc m)
  _∷ᵥ_ V M = V Vec.∷ M

  infixr 5 _∷ᵥ_

  -- A matrix of width 0
  []ᵥ : Matrix A 0 m
  []ᵥ = replicate _ []

  -- A matrix of height 0
  []ₕ : Matrix A n 0
  []ₕ = []

  -- The first column of a matrix
  headₕ : Matrix A (suc n) m → Vec A m
  headₕ = Vec.map Vec.head

  -- The first row of a matrix
  headᵥ : Matrix A n (suc m) → Vec A n
  headᵥ = head

  -- All but the first column of a matrix
  tailₕ : Matrix A (suc n) m → Matrix A n m
  tailₕ = Vec.map Vec.tail

  -- All but the first row of a matrix
  tailᵥ : Matrix A n (suc m) → Matrix A n m
  tailᵥ = tail

  -- View a matrix as a vector of rows
  rows : Matrix A n m → Vec (Vec A n) m
  rows = id

  -- View a matrix as a vector of columns
  columns : Matrix A n m → Vec (Vec A m) n
  columns {A = A} {n} = foldr (λ i → Vec (Vec A i) n) _∷ₕ_ []ᵥ

  -- Intepret a vector of rows as a matrix
  ∷ᵥⁿ : Vec (Vec A n) m → Matrix A n m
  ∷ᵥⁿ = id

  -- Interpret a vector of columns as a matrix
  ∷ₕⁿ : Vec (Vec A m) n → Matrix A n m
  ∷ₕⁿ = columns

-- Transpose
_ᵀ : Matrix A n m → Matrix A m n
_ᵀ = ∷ᵥⁿ ∘ columns

infix 10 _ᵀ

-- Apply a function to each row
mapₕ : (Vec A n → B) → Matrix A n m → Vec B m
mapₕ f M = Vec.map f (rows M)

-- Apply a function to each column
mapᵥ : (Vec A m → B) → Matrix A n m → Vec B n
mapᵥ f M = Vec.map f (columns M)

-- Horizontally flatten a vector of same-height matrices
∥ⁿ : Vec (Matrix A n m) p → Matrix A (p * n) m
∥ⁿ [] = []ᵥ
∥ⁿ (M ∷ Ms) = M ∥ ∥ⁿ Ms

-- Vertically flatten a vector of same-width matrices
≑ⁿ : Vec (Matrix A n m) p → Matrix A n (p * m)
≑ⁿ [] = []ₕ
≑ⁿ (M ∷ Ms) = M ≑ ≑ⁿ Ms

-- Flatten a matrix of matrices
join : Matrix (Matrix A p q) n m → Matrix A (n * p) (m * q)
join M = ≑ⁿ (mapₕ ∥ⁿ M)

opaque

  unfolding Matrix

  head-∷-tailᵥ : (M : Matrix A n (suc m)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
  head-∷-tailᵥ (_ ∷ _) = ≡.refl

  head-∷-tailₕ : (M : Matrix A (suc n) m) → headₕ M ∷ₕ tailₕ M ≡ M
  head-∷-tailₕ M = begin
      zipWith _∷_ (Vec.map Vec.head M) (Vec.map Vec.tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩
      Vec.map (λ x → head x ∷ tail x) M                     ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩
      Vec.map id M                                          ≡⟨ map-id M ⟩
      M ∎

  []ᵥ-! : (E : Matrix A 0 m) → E ≡ []ᵥ
  []ᵥ-! [] = ≡.refl
  []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E)

  []ᵥ-≑ : []ᵥ {m = n} ≑ []ᵥ ≡ []ᵥ {A = A} {n + m}
  []ᵥ-≑ {n = n} {m = m} = replicate-++ n m []

  []ᵥ-∥ : (M : Matrix A n m) → []ᵥ ∥ M ≡ M
  []ᵥ-∥ [] = ≡.refl
  []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M)

  ∷ₕ-∥ : (V : Vec A p) (M : Matrix A n p) (N : Matrix A m p) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N
  ∷ₕ-∥ [] [] [] = ≡.refl
  ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N)

  ∷ₕ-≑ : (V : Vec A n) (W : Vec A m) (M : Matrix A p n) (N : Matrix A p m) → (V ++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N)
  ∷ₕ-≑ [] W [] N = ≡.refl
  ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)

  ∷ᵥ-∥ : (V : Vec A n) (W : Vec A m) (M : Matrix A n p) (N : Matrix A m p) → (V ++ W) ∷ᵥ (M ∥ N) ≡ (V ∷ᵥ M) ∥ (W ∷ᵥ N)
  ∷ᵥ-∥ {_} {A} {n} {m} {p} V W M N = ≡.refl

  []ₕ-! : (E : Matrix A n 0) → E ≡ []ₕ
  []ₕ-! [] = ≡.refl

  []ₕ-≑ : (M : Matrix A n m) → []ₕ ≑ M ≡ M
  []ₕ-≑ _ = ≡.refl

  ∷ᵥ-≑ : (V : Vec A n) (M : Matrix A n m) (N : Matrix A n p) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N
  ∷ᵥ-≑ V M N = ≡.refl

  ≑-∥
      : (M : Matrix A n m)
        (N : Matrix A p m)
        (P : Matrix A n q)
        (Q : Matrix A p q)
      → M ∥ N ≑ P ∥ Q ≡ (M ≑ P) ∥ (N ≑ Q)
  ≑-∥ M N P Q = begin
      zipWith _++_ M N ++ zipWith _++_ P Q  ≡⟨ zipWith-++ _++_ M P N Q ⟨
      zipWith _++_ (M ++ P) (N ++ Q)        ∎

  columns-∷ₕ : (V : Vec A n) (M : Matrix A m n) → columns (V ∷ₕ M) ≡ V ∷ columns M
  columns-∷ₕ {A = A} {n} {m} [] [] = ≡.refl
  columns-∷ₕ {A = A} {n} {m} (x ∷ V) (M₀ ∷ M) = begin
      (x ∷ M₀) ∷ₕ (columns (V ∷ₕ M))  ≡⟨ ≡.cong ((x ∷ M₀) ∷ₕ_) (columns-∷ₕ V M) ⟩
      (x ∷ V) ∷ columns (M₀ ∷ M)      ∎

  columns-∥ : (M : Matrix A m p) (N : Matrix A n p) → columns (M ∥ N) ≡ columns M ++ columns N
  columns-∥ {m = m} {n = n} [] [] = ≡.sym (replicate-++ m n [])
  columns-∥ (M₀ ∷ M) (N₀ ∷ N) = begin
      zipWith _∷_ (M₀ ++ N₀) (columns (M ∥ N))                  ≡⟨ ≡.cong (zipWith _∷_ (M₀ ++ N₀)) (columns-∥ M N) ⟩
      zipWith _∷_ (M₀ ++ N₀) (columns M ++ columns N)           ≡⟨ zipWith-++ _∷_ M₀ N₀ (columns M) (columns N) ⟩
      zipWith _∷_ M₀ (columns M) ++ zipWith _∷_ N₀ (columns N)  ∎

  columns-≑ : (M : Matrix A m n) (N : Matrix A m p) → columns (M ≑ N) ≡ zipWith _++_ (columns M) (columns N)
  columns-≑ [] N = ≡.sym ([]ᵥ-∥ (columns N))
  columns-≑ (V ∷ M) N = begin
      zipWith _∷_ V (columns (M ++ N))                      ≡⟨ ≡.cong (zipWith _∷_ V) (columns-≑ M N) ⟩
      zipWith _∷_ V (zipWith _++_ (columns M) (columns N))  ≡⟨ ∷ₕ-∥ V (M ᵀ) (N ᵀ) ⟩
      zipWith _++_ (zipWith _∷_ V (columns M)) (columns N)  ∎

join-[]ᵥ : join ([]ᵥ {a} {Matrix A m p} {n}) ≡ []ᵥ
join-[]ᵥ = []ᵥ-! (join []ᵥ)

join-[]ₕ : join ([]ₕ {a} {Matrix A m p} {n}) ≡ []ₕ
join-[]ₕ = []ₕ-! (join []ₕ)

[]ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n}
[]ᵥ-ᵀ = []ₕ-! ([]ᵥ ᵀ)

opaque

  unfolding Matrix

  ∷ₕ-ᵀ : (V : Vec A n) (M : Matrix A m n) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ
  ∷ₕ-ᵀ V M = columns-∷ₕ V M

  ∷ᵥ-ᵀ : (V : Vec A m) (M : Matrix A m n) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ
  ∷ᵥ-ᵀ V M = ≡.refl

  _ᵀᵀ : (M : Matrix A n m) → M ᵀ ᵀ ≡ M
  _ᵀᵀ [] = []ᵥ-ᵀ
  _ᵀᵀ (M₀ ∷ M) = begin
      (M₀ ∷ₕ M ᵀ) ᵀ ≡⟨ ∷ₕ-ᵀ M₀ (M ᵀ)  ⟩
      M₀ ∷ᵥ M ᵀ ᵀ   ≡⟨ ≡.cong (M₀ ∷ᵥ_) (M ᵀᵀ) ⟩
      M₀ ∷ᵥ M       ∎

  infix 10 _ᵀᵀ

  ≑ⁿ-∥ : (Ms : Vec (Matrix A n p) q) (Ns : Vec (Matrix A m p) q) → ≑ⁿ (zipWith _∥_ Ms Ns) ≡ ≑ⁿ Ms ∥ ≑ⁿ Ns
  ≑ⁿ-∥ {n = n} [] [] = ≡.sym ([]ₕ-! ([]ₕ {n = n} ∥ []ₕ))
  ≑ⁿ-∥ (M ∷ Ms) (N ∷ Ns) = begin
      M ∥ N ≑ ≑ⁿ (zipWith _∥_ Ms Ns)  ≡⟨ ≡.cong (M ∥ N ≑_) (≑ⁿ-∥ Ms Ns) ⟩
      M ∥ N ≑ ≑ⁿ Ms ∥ ≑ⁿ Ns           ≡⟨ ≑-∥ M N (≑ⁿ Ms) (≑ⁿ Ns) ⟩
      (M ≑ ≑ⁿ Ms) ∥ (N ≑ ≑ⁿ Ns)       ∎

  join-∷ₕ : (V : Vec (Matrix A n m) q) (M : Matrix (Matrix A n m) p q) → join (V ∷ₕ M) ≡ ≑ⁿ V ∥ join M
  join-∷ₕ V M = begin
      ≑ⁿ (mapₕ ∥ⁿ (V ∷ₕ M))               ≡⟨ ≡.cong ≑ⁿ (map-zipWith ∥ⁿ _∷_ V M) ⟩
      ≑ⁿ (zipWith (λ x y → x ∥ ∥ⁿ y) V M) ≡⟨ ≡.cong ≑ⁿ (zipWith-map₂ _∥_ ∥ⁿ V M) ⟨
      ≑ⁿ (zipWith _∥_ V (mapₕ ∥ⁿ M))      ≡⟨ ≑ⁿ-∥ V (mapₕ ∥ⁿ M) ⟩
      ≑ⁿ V ∥ ≑ⁿ (mapₕ ∥ⁿ M)               ∎

  join-∷ᵥ : (V : Vec (Matrix A n m) p) (M : Matrix (Matrix A n m) p q) → join (V ∷ᵥ M) ≡ ∥ⁿ V ≑ join M
  join-∷ᵥ V M = ≡.refl

  ≑ⁿ-∷ₕ : (Vs : Vec (Vec A m) p) (Ms : Vec (Matrix A n m) p) → ≑ⁿ (zipWith _∷ₕ_ Vs Ms) ≡ concat Vs ∷ₕ ≑ⁿ Ms
  ≑ⁿ-∷ₕ [] [] = ≡.sym ([]ₕ-! ([] ∷ₕ []ₕ))
  ≑ⁿ-∷ₕ (V ∷ Vs) (M ∷ Ms) = begin
      (V ∷ₕ M) ≑ ≑ⁿ (zipWith _∷ₕ_ Vs Ms)  ≡⟨ ≡.cong ((V ∷ₕ M) ≑_) (≑ⁿ-∷ₕ Vs Ms) ⟩
      (V ∷ₕ M) ≑ (concat Vs ∷ₕ ≑ⁿ Ms)     ≡⟨ ∷ₕ-≑ V (concat Vs) M (≑ⁿ Ms) ⟨
      (V ++ concat Vs) ∷ₕ (M ≑ ≑ⁿ Ms)     ∎

  replicate-∷ₕ : (V : Vec A m) (M : Matrix A n m) → replicate p (V ∷ₕ M) ≡ zipWith _∷ₕ_ (replicate p V) (replicate p M)
  replicate-∷ₕ V M = ≡.sym (zipWith-replicate _∷ₕ_ V M)

  ≑ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ≑ⁿ (replicate p M) ≡ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M)
  ≑ⁿ-replicate {n = zero} p M = ≡.trans ([]ᵥ-! (≑ⁿ (replicate p M))) (≡.sym ([]ᵥ-! (∷ₕⁿ (mapᵥ (concat ∘ replicate p) M))))
  ≑ⁿ-replicate {n = suc n} p M = begin
      ≑ⁿ (replicate p M)                                                            ≡⟨ ≡.cong (≑ⁿ ∘ replicate p) (head-∷-tailₕ M) ⟨
      ≑ⁿ (replicate p (headₕ M ∷ₕ tailₕ M))                                         ≡⟨ ≡.cong ≑ⁿ (replicate-∷ₕ {p = p} (headₕ M) (tailₕ M)) ⟩
      ≑ⁿ (zipWith _∷ₕ_ (replicate p (headₕ M)) (replicate p (tailₕ M)))             ≡⟨ ≑ⁿ-∷ₕ (replicate p (headₕ M)) (replicate p (tailₕ M)) ⟩
      concat (replicate p (headₕ M)) ∷ₕ (≑ⁿ (replicate p (tailₕ M)))                ≡⟨ ≡.cong (concat (replicate p (headₕ M)) ∷ₕ_) (≑ⁿ-replicate p (tailₕ M)) ⟩
      concat (replicate p (headₕ M)) ∷ₕ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (tailₕ M)) ≡⟨ ≡.cong (∷ₕⁿ ∘ Vec.map (concat ∘ replicate p)) (∷ₕ-ᵀ (headₕ M) (tailₕ M)) ⟨
      ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (headₕ M ∷ₕ tailₕ M))                        ≡⟨ ≡.cong (∷ₕⁿ ∘ mapᵥ (concat ∘ replicate p)) (head-∷-tailₕ M) ⟩
      ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M)                                           ∎

  ∥ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ∥ⁿ (replicate p M) ≡ ∷ᵥⁿ (mapₕ (concat ∘ replicate p) M)
  ∥ⁿ-replicate zero M = ≡.sym (map-const M [])
  ∥ⁿ-replicate (suc p) M = begin
      zipWith _++_ M (∥ⁿ (replicate p M))                             ≡⟨ ≡.cong (zipWith _++_ M) (∥ⁿ-replicate p M) ⟩
      zipWith _++_ M (Vec.map (concat ∘ replicate p) M)               ≡⟨ ≡.cong (λ h → zipWith _++_ h (Vec.map (concat ∘ replicate p) M)) (map-id M) ⟨
      zipWith _++_ (Vec.map id M) (Vec.map (concat ∘ replicate p) M)  ≡⟨ zipWith-map id (concat ∘ replicate p) _++_ M ⟩
      Vec.map (λ V → V ++ concat (replicate p V)) M                   ∎

opaque

  unfolding ∷ₕⁿ

  columns-∷ₕⁿ : (Vs : Vec (Vec A n) m) → columns (∷ₕⁿ Vs) ≡ Vs
  columns-∷ₕⁿ Vs = Vs ᵀᵀ

  ∷ₕⁿ-columns : (M : Matrix A n m) → ∷ₕⁿ (columns M) ≡ M
  ∷ₕⁿ-columns M = M ᵀᵀ

  ∷ᵥⁿ-rows : (M : Matrix A n m) → ∷ᵥⁿ (rows M) ≡ M
  ∷ᵥⁿ-rows M = ≡.refl

  ∷ᵥⁿ-ᵀ : (Vs : Vec (Vec A n) m) → ∷ᵥⁿ Vs ᵀ ≡ ∷ₕⁿ Vs
  ∷ᵥⁿ-ᵀ Vs = ≡.refl

open Pointwise

module Natural (f : A → B) where

  open Vector.Natural

  opaque

    unfolding Matrix

    α-∥ : (M : Matrix A n p) (N : Matrix A m p) → map f (M ∥ N) ≡ map f M ∥ map f N
    α-∥ M N = begin
        Vec.map (Vec.map f) (zipWith _++_ M N)                        ≡⟨ map-zipWith (Vec.map f) _++_ M N ⟩
        zipWith (λ x y → Vec.map f (x ++ y)) M N                      ≡⟨ zipWith-cong (map-++ f) M N ⟩
        zipWith (λ x y → Vec.map f x ++ Vec.map f y) M N              ≡⟨ zipWith-map-map (Vec.map f) (Vec.map f) _++_ M N ⟩
        zipWith _++_ (Vec.map (Vec.map f) M) (Vec.map (Vec.map f) N)  ∎

    α-≑ : (M : Matrix A n m) (N : Matrix A n p) → map f (M ≑ N) ≡ map f M ≑ map f N
    α-≑ = map-++ (Vec.map f)

    α-∷ᵥ : (V : Vec A n) (M : Matrix A n m) → map f (V ∷ᵥ M) ≡ Vec.map f V ∷ᵥ map f M
    α-∷ᵥ _ _ = ≡.refl

    α-∷ₕ : (V : Vec A m) (M : Matrix A n m) → map f (V ∷ₕ M) ≡ Vec.map f V ∷ₕ map f M
    α-∷ₕ V M = begin
        Vec.map (Vec.map f) (zipWith _∷_ V M)             ≡⟨ map-zipWith (Vec.map f) _∷_ V M ⟩
        zipWith (λ x y → f x ∷ Vec.map f y) V M           ≡⟨ zipWith-map-map f (Vec.map f) _∷_ V M ⟩
        zipWith _∷_ (Vec.map f V) (Vec.map (Vec.map f) M) ∎

    α-headₕ : (M : Matrix A (suc n) m) → Vec.map f (headₕ M) ≡ headₕ (map f M)
    α-headₕ M = begin
        Vec.map f (Vec.map head M)            ≡⟨ map-∘ f head M ⟨
        Vec.map (f ∘ head) M                  ≡⟨ map-cong (α-head f) M ⟩
        Vec.map (head ∘ Vec.map f) M          ≡⟨ map-∘ head (Vec.map f) M ⟩
        Vec.map head (Vec.map (Vec.map f) M) ∎

    α-tailₕ : (M : Matrix A (suc n) m) → map f (tailₕ M) ≡ tailₕ (map f M)
    α-tailₕ M = begin
        Vec.map (Vec.map f) (Vec.map tail M)  ≡⟨ map-∘ (Vec.map f) tail M ⟨
        Vec.map (Vec.map f ∘ tail) M          ≡⟨ map-cong (α-tail f) M ⟩
        Vec.map (tail ∘ Vec.map f) M          ≡⟨ map-∘ tail (Vec.map f) M ⟩
        Vec.map tail (Vec.map (Vec.map f) M)  ∎

    α-[]ᵥ : map f ([]ᵥ {m = m}) ≡ []ᵥ
    α-[]ᵥ {m} = map-replicate (Vec.map f) [] m

    α-headᵥ : (M : Matrix A n (suc m)) → Vec.map f (headᵥ M) ≡ headᵥ (map f M)
    α-headᵥ = α-head (Vec.map f)

    α-tailᵥ : (M : Matrix A n (suc m)) → map f (tailᵥ M) ≡ tailᵥ (map f M)
    α-tailᵥ = α-tail (Vec.map f)

    α-[]ₕ : map f ([]ₕ {n = n}) ≡ []ₕ
    α-[]ₕ = ≡.refl

    α-ᵀ : (M : Matrix A n m) → map f (M ᵀ) ≡ map f M ᵀ
    α-ᵀ [] = α-[]ᵥ
    α-ᵀ (V ∷ M) = begin
        map f (V ∷ₕ M ᵀ)            ≡⟨ α-∷ₕ V (M ᵀ) ⟩
        Vec.map f V ∷ₕ map f (M ᵀ)  ≡⟨ ≡.cong (Vec.map f V ∷ₕ_) (α-ᵀ M) ⟩
        Vec.map f V ∷ₕ map f M ᵀ    ∎

module Relation {R : REL A B ℓ} where

  open Vector.Relation

  opaque

    unfolding PW

    R-∥ : {M₁ : Matrix A n p}
          {M₂ : Matrix B n p}
          {N₁ : Matrix A m p}
          {N₂ : Matrix B m p}
        → PW R M₁ M₂
        → PW R N₁ N₂
        → PW R (M₁ ∥ N₁) (M₂ ∥ N₂)
    R-∥ = R-zipWith {R = Pointwise R} (R-++ {R = R})

    R-≑ : {M₁ : Matrix A n m}
          {M₂ : Matrix B n m}
          {N₁ : Matrix A n p}
          {N₂ : Matrix B n p}
        → PW R M₁ M₂
        → PW R N₁ N₂
        → PW R (M₁ ≑ N₁) (M₂ ≑ N₂)
    R-≑ = R-++ {R = Pointwise R}

    R-∷ᵥ
        : {V₁ : Vec A n}
          {V₂ : Vec B n}
          {M₁ : Matrix A n m}
          {M₂ : Matrix B n m}
        → Pointwise R V₁ V₂
        → PW R M₁ M₂
        → PW R (V₁ ∷ᵥ M₁) (V₂ ∷ᵥ M₂)
    R-∷ᵥ R-V R-M = R-V ∷ R-M

    R-∷ₕ
        : {V₁ : Vec A n}
          {V₂ : Vec B n}
          {M₁ : Matrix A m n}
          {M₂ : Matrix B m n}
        → Pointwise R V₁ V₂
        → PW R M₁ M₂
        → PW R (V₁ ∷ₕ M₁) (V₂ ∷ₕ M₂)
    R-∷ₕ [] [] = []
    R-∷ₕ (R-x ∷ R-V) (R-M₀ ∷ R-M) = (R-x ∷ R-M₀) ∷ R-∷ₕ R-V R-M

    R-headₕ
        : {M₁ : Matrix A (suc n) m}
          {M₂ : Matrix B (suc n) m}
        → PW R M₁ M₂
        → Pointwise R (headₕ M₁) (headₕ M₂)
    R-headₕ = map⁺ R-head

    R-tailₕ
        : {M₁ : Matrix A (suc n) m}
          {M₂ : Matrix B (suc n) m}
        → PW R M₁ M₂
        → PW R (tailₕ M₁) (tailₕ M₂)
    R-tailₕ = map⁺ R-tail

    R-[]ᵥ : PW R []ᵥ ([]ᵥ {m = m})
    R-[]ᵥ = R-replicate []

    R-headᵥ
        : {M₁ : Matrix A n (suc m)}
          {M₂ : Matrix B n (suc m)}
        → PW R M₁ M₂
        → Pointwise R (headᵥ M₁) (headᵥ M₂)
    R-headᵥ = R-head

    R-tailᵥ
        : {M₁ : Matrix A n (suc m)}
          {M₂ : Matrix B n (suc m)}
        → PW R M₁ M₂
        → PW R (tailᵥ M₁) (tailᵥ M₂)
    R-tailᵥ = R-tail

    R-[]ₕ : PW R []ₕ ([]ₕ {n = n})
    R-[]ₕ = []

    R-ᵀ
        : {M₁ : Matrix A n m}
          {M₂ : Matrix B n m}
        → PW R M₁ M₂
        → PW R (M₁ ᵀ) (M₂ ᵀ)
    R-ᵀ [] = R-[]ᵥ
    R-ᵀ (R-V ∷ R-M) = R-∷ₕ R-V (R-ᵀ R-M)