Feature request: type aliases

[tonyxty]

Suppose I have defined functors and the category Set, and want to define contravariant functors and sheaves. Right now I can do this:

\class Functor (A B : Category) (F : A -> B)
  | fmap : -- ...
-- ...
\func ContravariantFunctor (C S : Category) : Category => Functor {C `opp} {S}
-- opp is the opposite category
\func Presheaf (C : Category) : Category => ContravariantFunctor C Category-Set
-- Category-Set is the category of sets

The problem is that many things possible with Functor {C `opp} Category-Set is not possible with Presheaf C. For example I can't say \new Presheaf C, I can't use \cowith with a \func declared to return Presheaf C, nor can I use F.fmap if F is declared a Presheaf.

I think it could be useful if we add type aliases for these partially applied types, much like Haskell's type keyword. Type aliases can be resolved early. In other words the following code should work:

\alias ContravariantFunctor (C S : Category) : Category => Functor {C `opp} {S}
\alias Presheaf (C : Category) : Category => ContravariantFunctor C Category-Set
\func PresheafFun (C : Category) (F : Presheaf C) : Presheaf C \cowith
  | fmap => F.fmap
  -- ...

[tonyxty]

So it's fixed now and no new keyword is required? Cool!