[Agda] Parameterized type families

[Nils Anders Danielsson]

Peter Berry wrote:

> 2008/10/22 Nils Anders Danielsson <nad at cs.nott.ac.uk>:
>
>> See the Agda wiki:
>> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.DatatypeAndFunctionDefinitions.
> 
> There's a little opaque type-theoretic jargon there. What does
> 'negative' mean? On the LHS of an arrow?

Negative:          To the left of an odd  number of arrows.
Positive:          To the left of an even number of arrows.
Strictly positive: To the left of zero              arrows.

> Presumably it's called that because it means its argument is being
> 'destroyed' or 'destructed', while on the RHS it's being 'created' or
> 'constructed' so is positive?

I do not know the etymology of this term.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.