Lists in HoTT

It seems like Lists in HoTT really want to be something like Σ[ n ∈ Nat ] Vec A n; this makes a lot of stuff much simpler. For instance, we can define thinnings of vectors xs : Vec A m, ys : Vec A n over thinnings f : m ⊑ n as ∀ (i : Fin m) → ys ! (f i) ≡ xs ! i; and this forms a nice cartesian fibration.

However, thinnings of fins are still weird, but can be clarified by thinking of them as a bundle over ℕ, ≤. Moreover, they are also a bundle over ℕ, < via strict thinnings.

-- Note that ≤ is the wrong notion here!
data Thinning : ∀ {m n : Nat} → m ≤ n → Fin (suc m) → Fin (suc n) → Type
  select : Thinning 0≤x fzero ?