From 6a35dcbbf1b3859b012e5f8546e8cb353898bde2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 2 Apr 2026 20:27:02 -0500
Subject: Reorganize matrix code

---
 Data/Vector/Core.agda | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

(limited to 'Data/Vector/Core.agda')

diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda
index 974f672..a430f12 100644
--- a/Data/Vector/Core.agda
+++ b/Data/Vector/Core.agda
@@ -13,18 +13,18 @@ open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; _+_)
 open import Data.Setoid using (∣_∣)
-open import Data.Vec using (Vec; lookup; tabulate)
+open import Data.Vec as Vec using (Vec; lookup; tabulate)
 open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
 open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
 open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open Func
 open Setoid S
-open Vec
 open Fin
+open Vec.Vec
 
 private
   variable
@@ -44,6 +44,18 @@ opaque
   ≊-isEquiv : IsEquivalence (_≊_ {n})
   ≊-isEquiv {n} = ≋-isEquivalence n
 
+  _++_ : Vector A → Vector B → Vector (A + B)
+  _++_ = Vec._++_
+
+  ⟨⟩ : Vector 0
+  ⟨⟩ = []
+
+  ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩
+  ⟨⟩-! [] = ≡.refl
+
+  ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V
+  ⟨⟩-++ V = ≡.refl
+
 -- A setoid of vectors for every natural number
 Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
 Vectorₛ n = record
-- 
cgit v1.2.3