Positivity annotations [Re: [Agda] parametrised data structures]

[Dan Doel]

On Thu, Jan 26, 2012 at 6:20 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> James' example is one more where one would want positivity annotations.
>  They are needed for compositional developments.
> A compositional type system allows to replace implementations by
> abstractions.  Agda lacks a few ingredients still, one of them is positivity
> annotations.

You want these for directed type theory, as well. You need to know
whether the hom type x ~> y induces F x ~> F y or F y ~> F x or
neither, etc.

If you want to be cutting edge.

-- Dan