Demisimplex Category

The demisimplex category is the Wide Subcategory of the Simplex Category consisting of only the degeneracies.

Inductive Representation

We can neatly encode the structure of the (augmented) demisimplex category with the following inductive.

data BlockVec {ℓ} (A : Type ℓ) : Nat → Nat → Type ℓ where
  [] : BlockVec A 0 0
  _∷_ : ∀ {m n} → A → BlockVec A (suc m) n → BlockVec A (suc (suc m)) n
  _❚_ : ∀ {m n} → A → BlockVec A m n → BlockVec A (suc m) (suc n)