Order of arguments to Vec is unexplained.

[kindaro]

On page 9, you define Vec thus:

data Vec (a :: *) (n :: Nat) where
    VNil  :: Vec a Zero
    VCons :: a -> Vec a n -> Vec a (Suc n)
infixr 5 ‘VCons‘

Then, on page 13, you proceed to discussing Applicative instance and lament that:

... we cannot make Vec an actual instance of the Applicative class: [t]he parameters of Vec are in the wrong order for that.

— But it was you who had chosen the order. It is not explained why this choice of order of arguments is still preferred, despite being adverse to the instantiation of usual classes.

I think it would be beneficial to either add some reasoning to this design choice, or defer the reader elsewhere.

[kosmikus]

Good point.