Type Function Aliases in Idris

Question

Is it possible to define a short alias of a type function in Idris?

While the following code type-checks, I'd like to have a shorter definition for AugentRow.

import Data.Vect

ColumnCount : Type
ColumnCount = Nat

Cell : Type
Cell = Type

Row : ColumnCount -> Cell -> Type
Row   columnCount    cell =  Vect columnCount cell

AugentRow : ColumnCount -> Cell -> Type
AugentRow   columnCount    cell =  Row columnCount cell

Some definition without unnessesory repetition like this one:

AugentRow = Row

Answer 1

The shortest form I've found so far:

AugentRow : ColumnCount -> Cell -> Type
AugentRow = Row