Thinnings

A thinning is a map in the (augmented) semisimplex category Ξ” + a subscript superscript Ξ” π‘Ž \Delta^{a}_{+} .

Note that a sort of "graded" thinning that keeps track of the number of variables thinned expresses a relational proof that d + m = n 𝑑 π‘š 𝑛 d+m=n . This is rather nice, as we can immediately tell if a thinning is an identity or not.

data Thinning : Nat β†’ Nat β†’ Nat β†’ Type where
  stop : Thinning 0 0 0
  keep : βˆ€ {d m n} β†’ Thinning d m n β†’ Thinning d (suc m) (suc n)
  skip : βˆ€ {d m n} β†’ Thinning d m n β†’ Thinning (suc d) m (suc n)

We also have a nice intuition for these as a sort of "zipper" of vectors; we can also think of the normal action of thinning on a vector as just adding "invisible" elements to the vector.

zipping : βˆ€ {β„“} {A : Type β„“} {m n o} β†’ Vec A m β†’ Vec A n β†’ Thinning m n o β†’ Vec A o
zipping xs ys stop⁺ = []
zipping xs (y ∷ ys) (keep⁺ th) = y ∷ zipping xs ys th
zipping (x ∷ xs) ys (skip⁺ th) = x ∷ zipping xs ys th