started sidebar for linarg correspondence

Makefile

@@ -1,5 +1,5 @@
-agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda) $(wildcard tspl/*.lagda) $(wildcard tspl/**/*.lagda)
-agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai) $(wildcard tspl/*.agdai) $(wildcard tspl/**/*.agdai)
+agda := $(shell find src tspl -type f -name '*.lagda')
+agdai := $(shell find src tspl -type f -name '*.agdai')
 markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/

src/plfa/Linearity.lagda

@@ -5,8 +5,7 @@ permalink : /Linearity/
 ---
 
 \begin{code}
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; refl; sym; cong)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 open import Algebra.Structures using (module IsSemiring; IsSemiring)
 \end{code}
 
@@ -15,15 +14,15 @@ module plfa.Linearity
   {Mult : Set}
   (_+_ _*_ : Mult → Mult → Mult)
   (0# 1# : Mult)
-  (+-*-isSemiring : IsSemiring _≡_ _+_ _*_ 0# 1#)
+  (*-+-isSemiring : IsSemiring _≡_ _+_ _*_ 0# 1#)
   where
 \end{code}
 
 \begin{code}
 open import Function using (_∘_; _|>_)
-open import Data.Product using (_×_; Σ-syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open Eq using (refl; sym; cong)
 open Eq.≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
-open IsSemiring +-*-isSemiring
+open IsSemiring *-+-isSemiring
   using (+-identityˡ; +-identityʳ; +-assoc; +-comm; *-identityˡ; *-identityʳ; *-assoc)
   renaming (zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ;
             distribˡ to *-distribˡ-+; distribʳ to *-distribʳ-+)
@@ -274,38 +273,13 @@ Precontext         ~>  ℕ
 Context γ          ~>  Vector γ
 γ ∋ A → Context δ  ~>  Matrix γ δ
 
+(See [this sidenote][plfa.Linearity.LinAlg].)
+
 \begin{code}
 Matrix : Precontext → Precontext → Set
 Matrix γ δ = ∀ {A} → γ ∋ A → Context δ
 \end{code}
 
-\begin{code}
-module Aside where
-
-  open import Data.Nat using (ℕ; suc; zero)
-  open import Data.Fin using (Fin; suc; zero)
-  open import Data.Vec using (Vec; _∷_; [])
-
-  ∥_∥ℕ : Precontext → ℕ
-  ∥ ∅     ∥ℕ = zero
-  ∥ γ , _ ∥ℕ = suc ∥ γ ∥ℕ
-
-  ∥_∥Fin : ∀ {γ} {A} → γ ∋ A → Fin ∥ γ ∥ℕ
-  ∥ Z   ∥Fin = zero
-  ∥ S x ∥Fin = suc ∥ x ∥Fin
-
-  ∥_∥Vec : ∀ {γ} → Context γ → Vec Mult ∥ γ ∥ℕ
-  ∥ ∅         ∥Vec = []
-  ∥ Γ , π ∙ _ ∥Vec = π ∷ ∥ Γ ∥Vec
-
-  Mat : Set → ℕ → ℕ → Set
-  Mat A n m = Vec (Vec A m) n
-
-  ∥_∥Mat : ∀ {γ δ} → Matrix γ δ → Mat Mult ∥ γ ∥ℕ ∥ δ ∥ℕ
-  ∥_∥Mat {∅}     {δ} Δ = []
-  ∥_∥Mat {γ , _} {δ} Δ = ∥ Δ Z ∥Vec ∷ ∥ (Δ ∘ S_) ∥Mat
-\end{code}
-
 \begin{code}
 identity : ∀ {γ} → Matrix γ γ
 identity {γ , A} Z     = 0s , 1# ∙ A

src/plfa/Linearity/LinAlg.lagda

@@ -0,0 +1,56 @@
+---
+title     : "Linearity: Resources and Linear Algebra"
+layout    : page
+permalink : /Linearity/LinAlg/
+---
+
+\begin{code}
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Algebra.Structures using (module IsSemiring; IsSemiring)
+\end{code}
+
+\begin{code}
+module plfa.Linearity.LinAlg
+  {Mult : Set}
+  (_+_ _*_ : Mult → Mult → Mult)
+  (0# 1# : Mult)
+  (*-+-isSemiring : IsSemiring _≡_ _+_ _*_ 0# 1#)
+  where
+\end{code}
+
+\begin{code}
+open import plfa.Linearity _+_ _*_ 0# 1# *-+-isSemiring
+open import Function using (_∘_)
+open import Data.Nat using (ℕ; suc; zero)
+open import Data.Fin using (Fin; suc; zero)
+open import Data.Vec using (Vec; _∷_; [])
+\end{code}
+
+\begin{code}
+∥_∥ℕ : Precontext → ℕ
+∥ ∅     ∥ℕ = zero
+∥ γ , _ ∥ℕ = suc ∥ γ ∥ℕ
+\end{code}
+
+\begin{code}
+∥_∥Fin : ∀ {γ} {A} → γ ∋ A → Fin ∥ γ ∥ℕ
+∥ Z   ∥Fin = zero
+∥ S x ∥Fin = suc ∥ x ∥Fin
+\end{code}
+
+\begin{code}
+∥_∥Vec : ∀ {γ} → Context γ → Vec Mult ∥ γ ∥ℕ
+∥ ∅         ∥Vec = []
+∥ Γ , π ∙ _ ∥Vec = π ∷ ∥ Γ ∥Vec
+\end{code}
+
+\begin{code}
+Mat : Set → ℕ → ℕ → Set
+Mat A n m = Vec (Vec A m) n
+\end{code}
+
+\begin{code}
+∥_∥Mat : ∀ {γ δ} → Matrix γ δ → Mat Mult ∥ γ ∥ℕ ∥ δ ∥ℕ
+∥_∥Mat {∅}     {δ} Δ = []
+∥_∥Mat {γ , _} {δ} Δ = ∥ Δ Z ∥Vec ∷ ∥ (Δ ∘ S_) ∥Mat
+\end{code}