refactor: use a refinement type for Data.Vec

resolves: #567

Co-authored-by: Reed Mullanix <reedmullanix@gmail.com>

Author: 4e554c4c

src/1Lab/Reflection.lagda.md

@@ -31,7 +31,7 @@ open import Meta.Alt public
 
 open Data.Product.NAry using ([_]) public
 open Data.List.Base hiding (lookup ; tabulate) public
-open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
+open Data.Vec.Base hiding (_++_ ; tail ; head; zero; suc) public
 open Data.Bool.Base public
 open Data.Dec.Base public
 

src/1Lab/Reflection/Deriving/Show.agda

@@ -9,7 +9,7 @@ open import Data.String.Show
 open import Data.String.Base
 open import Data.Char.Base
 open import Data.Fin.Base
-open import Data.Vec.Base hiding (map)
+open import Data.Vec.Base
 open import Data.Nat.Base
 open import Data.Int.Base using (Int ; pos ; negsuc)
 

src/1Lab/Reflection/List.lagda.md

@@ -184,12 +184,11 @@ not-member! {not-mem = not-mem} = not-mem
 
 ```agda
 private
-  member-example : true ∈ [ false , true , false , true , false ]
+  member-example : true ∈ [ false , true , false , true , false ]L
   member-example = member!
-
-  not-member-example : true ∉ [ false , false , false ]
+  not-member-example : true ∉ [ false , false , false ]L
   not-member-example = not-member!
 
-  unique-member-example : is-contr (true ∈ [ false , true , false , false ])
+  unique-member-example : is-contr (true ∈ [ false , true , false , false ]L)
   unique-member-example = unique-member!
 ```

src/1Lab/Reflection/Variables.agda

@@ -81,7 +81,7 @@ private
   env-rec Mot _▷*_ []* (xs ▷ x) = env-rec (Mot ∘ suc) _▷*_ ([]* ▷* x) xs
 
   reverse : Env A n → Vec A n
-  reverse {A = A} env = env-rec (Vec A) (λ xs x → x ∷ xs) [] env
+  reverse {A = A} env = env-rec (Vec A) (λ xs x → x ∷v xs) []v env
 
 
 

src/Algebra/Ring/Solver.agda

@@ -73,7 +73,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   En : ∀ {n} → Normal n → Vec R n → R
 
   Ep ∅ i = R.0r
-  Ep (p *x+ c) (x ∷ e) = Ep p (x ∷ e) R.* x R.+ En c e
+  Ep (p *x+ c) v with (x ∷ e) ← vec-view v = Ep p (x ∷v e) R.* x R.+ En c e
 
   En (con x) i = embed-coe x
   En (poly x) i = Ep x i
@@ -234,32 +234,34 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   ⟦ x ⟧ₙ ρ = En (normal x) ρ
 
   0n-hom : ∀ {n} (ρ : Vec R n) → En 0n ρ ≡ R.0r
-  0n-hom [] = ℤ↪R.pres-0
-  0n-hom (x ∷ ρ) = refl
+  0n-hom v with vec-view v
+  ... | [] = ℤ↪R.pres-0
+  ... | (x ∷ ρ) = refl
 
   1n-hom : ∀ {n} (ρ : Vec R n) → En 1n ρ ≡ R.1r
-  1n-hom [] = ℤ↪R.pres-id
-  1n-hom (x ∷ ρ) =
+  1n-hom v with vec-view v
+  ... | [] = ℤ↪R.pres-id
+  ... | (x ∷ ρ) =
     (R.0r R.* x) R.+ (En 1n ρ) ≡⟨ R.eliml R.*-zerol ⟩
     En 1n ρ                    ≡⟨ 1n-hom ρ ⟩
     R.1r                       ∎
 
   *x+ₙ-sound
     : ∀ {n} (p : Poly (suc n)) (c : Normal n) ρ
     → Ep (p *x+ₙ c) ρ ≡ Ep (p *x+ c) ρ
-  *x+ₙ-sound ∅ c (e ∷ ρ) with c ==ₙ 0n
-  ... | just x = sym $
-    Ep (∅ *x+ ⌜ c ⌝) (e ∷ ρ)   ≡⟨ ap! x ⟩
-    Ep (∅ *x+ 0n) (e ∷ ρ)      ≡⟨⟩
+  *x+ₙ-sound ∅ c v with vec-view v | c ==ₙ 0n
+  ... | (e ∷ ρ) | just x = sym $
+    Ep (∅ *x+ ⌜ c ⌝) (e ∷v ρ)   ≡⟨ ap! x ⟩
+    Ep (∅ *x+ 0n) (e ∷v ρ)      ≡⟨⟩
     (R.0r R.* e) R.+ En 0n ρ ≡⟨ R.eliml R.*-zerol ⟩
     En 0n ρ                  ≡⟨ 0n-hom ρ ⟩
     R.0r                               ∎
-  ... | nothing = refl
+  ... | (e ∷ ρ) | nothing = refl
   *x+ₙ-sound (p *x+ x) c ρ = refl
 
   ∅*x+ₙ-hom
     : ∀ {n} (c : Normal n) x ρ
-    → Ep (∅ *x+ₙ c) (x ∷ ρ) ≡ En c ρ
+    → Ep (∅ *x+ₙ c) (x ∷v ρ) ≡ En c ρ
   ∅*x+ₙ-hom c x ρ with c ==ₙ 0n
   ... | just x = sym (ap (λ c → En c ρ) x ∙ 0n-hom ρ)
   ... | nothing = R.eliml R.*-zerol
@@ -273,48 +275,48 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
 
   +ₚ-hom ∅ q ρ = sym R.+-idl
   +ₚ-hom (p *x+ x) ∅ ρ = sym R.+-idr
-  +ₚ-hom (p *x+ c) (q *x+ d) (x ∷ ρ) =
-    Ep ((p +ₚ q) *x+ₙ (c +ₙ d)) (x ∷ ρ)                                 ≡⟨ *x+ₙ-sound (p +ₚ q) (c +ₙ d) (x ∷ ρ) ⟩
-    Ep ((p +ₚ q) *x+ (c +ₙ d)) (x ∷ ρ)                                  ≡⟨⟩
-    ⌜ Ep (p +ₚ q) (x ∷ ρ) ⌝ R.* x R.+ En (c +ₙ d) ρ                     ≡⟨ ap! (+ₚ-hom p q (x ∷ ρ)) ⟩
-    (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x R.+ ⌜ En (c +ₙ d) ρ ⌝         ≡⟨ ap! (+ₙ-hom c d ρ) ⟩
-    ⌜ (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x ⌝ R.+ (En c ρ R.+ En d ρ)   ≡⟨ ap! R.*-distribr  ⟩
-    Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ) R.* x R.+ (En c ρ R.+ En d ρ)   ≡⟨ R.a.pullr (R.pulll R.+-commutes) ⟩
-    Ep p (x ∷ ρ) R.* x R.+ (En c ρ R.+ Ep q (x ∷ ρ) R.* x R.+ En d ρ)   ≡⟨ R.a.extendl (R.a.pulll refl) ⟩
-    Ep p (x ∷ ρ) R.* x R.+ En c ρ R.+ (Ep q (x ∷ ρ) R.* x R.+ En d ρ)   ∎
+  +ₚ-hom (p *x+ c) (q *x+ d) v with (x ∷ ρ) ← vec-view v =
+    Ep ((p +ₚ q) *x+ₙ (c +ₙ d)) (x ∷v ρ)                                ≡⟨ *x+ₙ-sound (p +ₚ q) (c +ₙ d) (x ∷v ρ) ⟩
+    Ep ((p +ₚ q) *x+ (c +ₙ d)) (x ∷v ρ)                                 ≡⟨⟩
+    ⌜ Ep (p +ₚ q) (x ∷v ρ) ⌝ R.* x R.+ En (c +ₙ d) ρ                    ≡⟨ ap! (+ₚ-hom p q (x ∷v ρ)) ⟩
+    (Ep p (x ∷v ρ) R.+ Ep q (x ∷v ρ)) R.* x R.+ ⌜ En (c +ₙ d) ρ ⌝       ≡⟨ ap! (+ₙ-hom c d ρ) ⟩
+    ⌜ (Ep p (x ∷v ρ) R.+ Ep q (x ∷v ρ)) R.* x ⌝ R.+ (En c ρ R.+ En d ρ) ≡⟨ ap! R.*-distribr  ⟩
+    Ep p (x ∷v ρ) R.* x R.+ Ep q (x ∷v ρ) R.* x R.+ (En c ρ R.+ En d ρ) ≡⟨ R.a.pullr (R.pulll R.+-commutes) ⟩
+    Ep p (x ∷v ρ) R.* x R.+ (En c ρ R.+ Ep q (x ∷v ρ) R.* x R.+ En d ρ) ≡⟨ R.a.extendl (R.a.pulll refl) ⟩
+    Ep p (x ∷v ρ) R.* x R.+ En c ρ R.+ (Ep q (x ∷v ρ) R.* x R.+ En d ρ) ∎
   +ₙ-hom (con x)  (con y)  ρ = ℤ↪R.pres-+ (lift x) (lift y)
   +ₙ-hom (poly p) (poly q) ρ = +ₚ-hom p q ρ
 
   *x+-hom
     : ∀ {n} (p q : Poly (suc n)) x ρ
-    → Ep (p *x+ₚ q) (x ∷ ρ)
-    ≡ Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ)
+    → Ep (p *x+ₚ q) (x ∷v ρ)
+    ≡ Ep p (x ∷v ρ) R.* x R.+ Ep q (x ∷v ρ)
   *x+-hom ∅ ∅ x ρ = R.introl R.*-zerol
   *x+-hom (p *x+ c) ∅ x ρ = ap₂ R._+_ refl (0n-hom ρ)
   *x+-hom p (q *x+ d) x ρ =
-    Ep (p *x+ₚ (q *x+ d)) (x ∷ ρ)                          ≡⟨⟩
-    Ep ((p +ₚ q) *x+ₙ d) (x ∷ ρ)                           ≡⟨ *x+ₙ-sound (p +ₚ q) d (x ∷ ρ) ⟩
-    ⌜ Ep (p +ₚ q) (x ∷ ρ) ⌝ R.* x R.+ En d ρ               ≡⟨ ap! (+ₚ-hom p q (x ∷ ρ)) ⟩
-    ⌜ (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x ⌝ R.+ En d ρ   ≡⟨ ap! R.*-distribr ⟩
-    Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ) R.* x R.+ En d ρ   ≡⟨ R.pullr refl ⟩
-    Ep p (x ∷ ρ) R.* x R.+ (Ep q (x ∷ ρ) R.* x R.+ En d ρ) ∎
+    Ep (p *x+ₚ (q *x+ d)) (x ∷v ρ)                           ≡⟨⟩
+    Ep ((p +ₚ q) *x+ₙ d) (x ∷v ρ)                            ≡⟨ *x+ₙ-sound (p +ₚ q) d (x ∷v ρ) ⟩
+    ⌜ Ep (p +ₚ q) (x ∷v ρ) ⌝ R.* x R.+ En d ρ                ≡⟨ ap! (+ₚ-hom p q (x ∷v ρ)) ⟩
+    ⌜ (Ep p (x ∷v ρ) R.+ Ep q (x ∷v ρ)) R.* x ⌝ R.+ En d ρ   ≡⟨ ap! R.*-distribr ⟩
+    Ep p (x ∷v ρ) R.* x R.+ Ep q (x ∷v ρ) R.* x R.+ En d ρ   ≡⟨ R.pullr refl ⟩
+    Ep p (x ∷v ρ) R.* x R.+ (Ep q (x ∷v ρ) R.* x R.+ En d ρ) ∎
 
   *ₙₚ-hom
     : ∀ {n} (c : Normal n) (p : Poly (suc n)) x ρ
-    → Ep (c *ₙₚ p) (x ∷ ρ) ≡ En c ρ R.* Ep p (x ∷ ρ)
+    → Ep (c *ₙₚ p) (x ∷v ρ) ≡ En c ρ R.* Ep p (x ∷v ρ)
   *ₚₙ-hom
     : ∀ {n} (c : Normal n) (p : Poly (suc n)) x ρ
-    → Ep (p *ₚₙ c) (x ∷ ρ) ≡ Ep p (x ∷ ρ) R.* En c ρ
+    → Ep (p *ₚₙ c) (x ∷v ρ) ≡ Ep p (x ∷v ρ) R.* En c ρ
   *ₙ-hom : ∀ {n} (c d : Normal n) ρ → En (c *ₙ d) ρ ≡ En c ρ R.* En d ρ
   *ₚ-hom : ∀ {n} (p q : Poly (suc n)) ρ → Ep (p *ₚ q) ρ ≡ Ep p ρ R.* Ep q ρ
 
   *ₚ-hom ∅ q ρ = sym R.*-zerol
   *ₚ-hom (p *x+ c) ∅ ρ = sym R.*-zeror
-  *ₚ-hom (p *x+ c) (q *x+ d) (x ∷ ρ) =
-      *x+ₙ-sound ((p *ₚ q) *x+ₚ ((p *ₚₙ d) +ₚ (c *ₙₚ q))) _ (x ∷ ρ)
+  *ₚ-hom (p *x+ c) (q *x+ d) v with (x ∷ ρ) ← vec-view v =
+      *x+ₙ-sound ((p *ₚ q) *x+ₚ ((p *ₚₙ d) +ₚ (c *ₙₚ q))) _ (x ∷v ρ)
     ∙ ap₂ R._+_ (ap₂ R._*_ (*x+-hom (p *ₚ q) ((p *ₚₙ d) +ₚ (c *ₙₚ q)) x ρ) refl) refl
-    ∙ ap₂ R._+_ (ap₂ R._*_ (ap₂ R._+_ (ap (R._* x) (*ₚ-hom p q (x ∷ ρ)))
-        (+ₚ-hom (p *ₚₙ d) (c *ₙₚ q) (x ∷ ρ))) refl
+    ∙ ap₂ R._+_ (ap₂ R._*_ (ap₂ R._+_ (ap (R._* x) (*ₚ-hom p q (x ∷v ρ)))
+        (+ₚ-hom (p *ₚₙ d) (c *ₙₚ q) (x ∷v ρ))) refl
         ∙ ap₂ R._*_ (ap₂ R._+_ refl (ap₂ R._+_ (*ₚₙ-hom d p x ρ) (*ₙₚ-hom c q x ρ)))
         refl) refl
     ∙ ap₂ R._+_ refl (*ₙ-hom c d ρ) ∙ lemma _ _ _ _ _
@@ -372,26 +374,27 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   -ₚ-hom : ∀ {n} (p : Poly (suc n)) ρ → Ep (-ₚ p) ρ ≡ R.- Ep p ρ
   -ₙ-hom : ∀ {n} (n : Normal n) ρ → En (-ₙ n) ρ ≡ R.- En n ρ
 
-  -ₚ-hom p (x ∷ ρ) =
-      *ₙₚ-hom (-ₙ 1n) p x ρ
+  -ₚ-hom p v with (x ∷ ρ) ← vec-view v =
+    *ₙₚ-hom (-ₙ 1n) p x ρ
     ∙ ap₂ R._*_ (-ₙ-hom 1n ρ ∙ ap R.-_ (1n-hom ρ)) refl
     ∙ R.*-negatel ∙ ap R.-_ R.*-idl
   -ₙ-hom (con x) ρ = ℤ↪R.pres-neg {x = lift x}
   -ₙ-hom (poly x) ρ = -ₚ-hom x ρ
 
   sound-coe
     : ∀ {n} (c : Int) (ρ : Vec R n) → En (normal-coe c) ρ ≡ embed-coe c
-  sound-coe c [] = refl
-  sound-coe c (x ∷ ρ) = ∅*x+ₙ-hom (normal-coe c) x ρ ∙ sound-coe c ρ
+  sound-coe c v with vec-view v
+  ... | [] = refl
+  ... | (x ∷ ρ) = ∅*x+ₙ-hom (normal-coe c) x ρ ∙ sound-coe c ρ
 
   sound-var : ∀ {n} (j : Fin n) ρ → En (normal-var j) ρ ≡ lookup ρ j
-  sound-var i _ with fin-view i
-  sound-var _ (x ∷ ρ) | zero =
-    Ep (∅ *x+ 1n) (x ∷ ρ) R.* x R.+ En 0n ρ ≡⟨ R.elimr (0n-hom ρ) ⟩
-    ⌜ Ep (∅ *x+ 1n) (x ∷ ρ) ⌝ R.* x         ≡⟨ ap! (R.eliml R.*-zerol ∙ 1n-hom ρ) ⟩
-    R.1r R.* x                              ≡⟨ R.*-idl ⟩
-    x                                       ∎
-  sound-var _ (x ∷ ρ) | suc j = ∅*x+ₙ-hom (normal-var j) x ρ ∙ sound-var j ρ
+  sound-var i v with vec-view v | fin-view i
+  ... | (x ∷ ρ) | zero =
+    Ep (∅ *x+ 1n) (x ∷v ρ) R.* x R.+ En 0n ρ ≡⟨ R.elimr (0n-hom ρ) ⟩
+    ⌜ Ep (∅ *x+ 1n) (x ∷v ρ) ⌝ R.* x         ≡⟨ ap! (R.eliml R.*-zerol ∙ 1n-hom ρ) ⟩
+    R.1r R.* x                               ≡⟨ R.*-idl ⟩
+    x                                        ∎
+  ... | (x ∷ ρ) | suc j = ∅*x+ₙ-hom (normal-var j) x ρ ∙ sound-var j ρ
 
   sound : ∀ {n} (p : Polynomial n) ρ → En (normal p) ρ ≡ ⟦ p ⟧ ρ
   sound (op [+] p q) ρ = +ₙ-hom (normal p) (normal q) ρ ∙ ap₂ R._+_ (sound p ρ) (sound q ρ)
@@ -411,11 +414,11 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   private
     test-distrib : ∀ x y z → x R.* (y R.+ z) ≡ y R.* x R.+ z R.* x
     test-distrib x y z =
-      solve (var 0 :* (var 1 :+ var 2)) ((var 1 :* var 0) :+ (var 2 :* var 0)) (x ∷ y ∷ z ∷ []) refl
+      solve (var 0 :* (var 1 :+ var 2)) ((var 1 :* var 0) :+ (var 2 :* var 0)) ([ x , y , z ]) refl
 
     test-identities : ∀ x → x R.+ (R.0r R.* R.1r) ≡ (R.1r R.+ R.0r) R.* x
     test-identities x =
-      solve (var 0 :+ (con 0 :* con 1)) ((con 1 :+ con 0) :* var 0) (x ∷ []) refl
+      solve (var 0 :+ (con 0 :* con 1)) ((con 1 :+ con 0) :* var 0) [ x ] refl
 
 module Explicit {ℓ} (R : CRing ℓ) where
   private module I = Impl (R .snd)

src/Cat/Instances/Assemblies.lagda.md

@@ -330,7 +330,7 @@ x$ is that $e$ is defined, and assemblies are defined so that if $e
   extend {X = X} f = to-assembly-hom record where
     map x     = f x
     realiser  = val ⟨ x ⟩ x
-    tracks ha = subst ⌞_⌟ (sym (abs-β _ [] (_ , X .def ha))) (X .def ha)
+    tracks ha = subst ⌞_⌟ (sym (abs-β _ []v (_ , X .def ha))) (X .def ha)
 ```
 
 <details>

src/Cat/Instances/Assemblies/Exponentials.lagda.md

@@ -8,7 +8,7 @@ open import Cat.Prelude
 
 open import Data.Partial.Total
 open import Data.Partial.Base
-open import Data.Vec.Base using ([] ; _∷_)
+open import Data.Vec.Base using ([]v ; _∷v_)
 
 open import Realisability.PCA
 
@@ -93,7 +93,7 @@ asm-ev {X = X} {Y = Y} = to-assembly-hom record where
   realiser = val ⟨ u ⟩ `fst `· u `· (`snd `· u)
 
   tracks {a = x} = elim! λ p q α pp p⊩f q⊩a → subst⊩ Y (p⊩f _ _ q⊩a) $
-    (val ⟨ u ⟩ `fst `· u `· (`snd `· u)) ⋆ x           ≡⟨ abs-β _ [] (_ , subst ⌞_⌟ (sym α) (`pair↓₂ pp (X .def q⊩a))) ⟩
+    (val ⟨ u ⟩ `fst `· u `· (`snd `· u)) ⋆ x           ≡⟨ abs-β _ []v (_ , subst ⌞_⌟ (sym α) (`pair↓₂ pp (X .def q⊩a))) ⟩
     `fst ⋆ ⌜ x ⌝ ⋆ (`snd ⋆ ⌜ x ⌝)                      ≡⟨ ap! α ⟩
     `fst ⋆ (`pair ⋆ p ⋆ q) ⋆ (`snd ⋆ (`pair ⋆ p ⋆ q))  ≡⟨ ap₂ _%_ (`fst-β pp (X .def q⊩a)) (`snd-β pp (X .def q⊩a)) ⟩
     p ⋆ q                                              ∎
@@ -120,7 +120,7 @@ curry-asm {X = X} {Y = Y} {Z = Z} h .map x = record where
       realiser = val ⟨ v ⟩ `h `· (`pair `· const (u , X .def u⊩x) `· v)
 
       tracks a⊩x = subst⊩ Z (t (inc (u , _ , refl , u⊩x , a⊩x))) $
-        abs-β _ [] (_ , Y .def a⊩x)
+        abs-β _ []v (_ , Y .def a⊩x)
 ```
 -->
 
@@ -137,9 +137,9 @@ curry-asm {X = X} {Y = Y} {Z = Z} h .tracked = do
     realiser = val ⟨ u ⟩ ⟨ v ⟩ `h `· (`pair `· u `· v)
 
     tracks a⊩x = record where
-      fst = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , X .def a⊩x) ∷ []))) (abs↓ _ _)
+      fst = subst ⌞_⌟ (sym (abs-βₙ []v ((_ , X .def a⊩x) ∷v []v))) (abs↓ _ _)
       snd = inc λ y b b⊩y → subst⊩ Z (t (inc (_ , _ , refl , a⊩x , b⊩y))) $
-        abs-βₙ [] ((b , Y .def b⊩y) ∷ (_ , X .def a⊩x) ∷ [])
+        abs-βₙ []v ((b , Y .def b⊩y) ∷v (_ , X .def a⊩x) ∷v []v)
 ```
 
 <details>

src/Cat/Instances/Assemblies/Limits.lagda.md

@@ -10,7 +10,7 @@ open import Cat.Prelude
 
 open import Data.Partial.Total
 open import Data.Partial.Base
-open import Data.Vec.Base using ([] ; _∷_)
+open import Data.Vec.Base using ([]v ; _∷v_)
 
 open import Realisability.PCA
 
@@ -156,7 +156,7 @@ tracked by the constant function with value $\sf{x}$.
 !Asm {X = X} = to-assembly-hom record where
   map    _  = lift tt
   realiser  = val ⟨ x ⟩ x
-  tracks ha = subst ⌞_⌟ (sym (abs-β _ [] (_ , X .def ha))) (X .def ha)
+  tracks ha = subst ⌞_⌟ (sym (abs-β _ []v (_ , X .def ha))) (X .def ha)
 ```
 
 <!--
@@ -191,7 +191,7 @@ Assemblies-equalisers f g .apex = Equ-asm f g
 Assemblies-equalisers {a = A} f g .equ = to-assembly-hom record where
   map (x , _) = x
   realiser    = val ⟨ x ⟩ x
-  tracks ha   = subst⊩ A ha (abs-β _ [] (_ , A .def ha))
+  tracks ha   = subst⊩ A ha (abs-β _ []v (_ , A .def ha))
 Assemblies-equalisers f g .has-is-eq .equal = ext λ x p → p
 ```
 

src/Data/List/Base.lagda.md

@@ -9,13 +9,16 @@ open import Data.Maybe.Base
 open import Data.Bool.Base
 open import Data.Dec.Base
 open import Data.Fin.Base
+open import Data.Irr
 
 open import Meta.Traversable
 open import Meta.Foldable
 open import Meta.Append
 open import Meta.Idiom
 open import Meta.Bind
 open import Meta.Alt
+
+import Data.Nat.Base as Nat
 ```
 -->
 
@@ -62,6 +65,9 @@ instance
     go (suc zero) xs          = xs ∷ []
     go (suc (suc n)) (x , xs) = x ∷ go (suc n) xs
 
+[_]L : ∀ {ℓ} {A : Type ℓ} {n} → Vecₓ A n → List A
+[ p ]L = [ p ]
+
 -- Test:
 _ : Path (List Nat) [ 1 , 2 , 3 ] (1 ∷ 2 ∷ 3 ∷ [])
 _ = refl
@@ -335,10 +341,18 @@ lookup x ((k , v) ∷ xs) with x ≡? k
 ... | yes _ = just v
 ... | no  _ = lookup x xs
 
+_!?_ : List A → Nat → Maybe A
+[] !? n = nothing
+(x ∷ xs) !? zero = just x
+(x ∷ xs) !? suc n = xs !? n
+
+!?-just : ∀ (xs : List A) (n : Nat) → (n Nat.< length xs) → is-just (xs !? n)
+!?-just {A = a} (x ∷ xs) zero n<xs = lift oh
+!?-just {A = a} (x ∷ xs) (suc n) n<xs = !?-just xs n (Nat.≤-peel n<xs)
+
 _!_ : (l : List A) → Fin (length l) → A
-(x ∷ xs) ! n with fin-view n
-... | zero  = x
-... | suc i = xs ! i
+xs ! (fin n ⦃ pf ⦄) = from-just! _ $ !?-just xs n pf
+
 
 tabulate : ∀ {n} (f : Fin n → A) → List A
 tabulate {n = zero}  f = []

src/Data/List/Sigma.agda

@@ -49,11 +49,11 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} where
       p b q q'
 
     rem₁ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibre' (ys x) p b → fibreᵢ (ys a !_) b
-    rem₁ {x = x} {a} ys b p (fin ix ⦃ q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.to (rem₀ ys b p ix) r where
+    rem₁ {x = x} {a} ys b p (fin ix ⦃ q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.to (rem₀ ys b p ix {q} {q'} ) r where
       q' = transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p (~ i)))) q
 
     rem₂ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibreᵢ (ys a !_) b → fibre' (ys x) p b
-    rem₂ {x = x} {a} ys b p (fin ix ⦃ q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.from (rem₀ ys b p ix) r where
+    rem₂ {x = x} {a} ys b p (fin ix ⦃ q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.from (rem₀ ys b p ix {q'} {q}) r where
       q' = transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p i))) q
 
   sigma-member : ∀ {a b xs ys} → a ∈ₗ xs → b ∈ₗ ys a → (a , b) ∈ₗ sigma xs ys