matrices.agda

{-# OPTIONS --safe --cubical #-}

module Bits where

open import Cubical.Data.Nat as ℕ using (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function

variable
  a : Level
  A : Set a

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

infixr 5 _∷_
data Vec (A : Set a) : ℕ → Set a where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

Vec′ : Set a → ℕ → Set a
Vec′ A n = Fin n → A

_[_] : ∀ {n} → Vec A n → Vec′ A n
(x ∷ xs) [ zero  ] = x
(x ∷ xs) [ suc i ] = xs [ i ]

tabulate : ∀ {n} → Vec′ A n → Vec A n
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)

open import Cubical.Foundations.Prelude

v→tab→v : ∀ {n} → (xs : Vec A n) → tabulate (_[_] xs) ≡ xs
v→tab→v [] = refl
v→tab→v (x ∷ xs) = cong (x ∷_) (v→tab→v xs)

tab→v→tab′ : ∀ {n} → (xs : Vec′ A n) → ∀ i → tabulate xs [ i ] ≡ xs i
tab→v→tab′ xs zero = refl
tab→v→tab′ xs (suc i) = tab→v→tab′ (xs ∘ suc) i

tab→v→tab : ∀ {n} → (xs : Vec′ A n) → _[_] (tabulate xs) ≡ xs
tab→v→tab xs = funExt (tab→v→tab′ xs)

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Core.Glue

Vec≃Vec′ : ∀ {n} → Vec A n ≃ Vec′ A n
Vec≃Vec′ = isoToEquiv (iso _[_] tabulate tab→v→tab v→tab→v)

record Semiring ℓ : Set (ℓ-suc ℓ) where
  infixl 6 _+_
  infixl 7 _×_
  field
    Carrier : Set ℓ
    _+_ : Carrier → Carrier → Carrier
    _×_ : Carrier → Carrier → Carrier
    0# : Carrier
    1# : Carrier

module Matrices {ℓ} (rng : Semiring ℓ) where
  open Semiring rng

  Mat : ℕ → ℕ → Set ℓ
  Mat n m = Vec′ (Vec′ Carrier m) n

  0ᵐ : ∀ {n m} → Mat n m
  0ᵐ _ _ = 0#

  1ᵐ : ∀ {n m} → Mat n m
  1ᵐ zero zero = 1#
  1ᵐ zero (suc _) = 0#
  1ᵐ (suc _) zero = 0#
  1ᵐ (suc i) (suc j) = 1ᵐ i j

  _+ᵐ_ : ∀ {n m} → Mat n m → Mat n m → Mat n m
  (xs +ᵐ ys) i j = xs i j + ys i j

  infix 2 Sum
  Sum : (n : ℕ) → (Fin n → Carrier) → Carrier
  Sum zero f = 0#
  Sum (suc n) f = f zero + Sum n (f ∘ suc)

  syntax Sum m (λ k → e) = Σ[ k ≡0][ m ] e

  _×ᵐ_ : ∀ {n m p} → Mat n m → Mat m p → Mat n p
  (xs ×ᵐ ys) i j = Σ[ k ≡0][ _ ] xs i k × ys k j