[Agda] Setω and abstraction

[Nils Anders Danielsson]

On 2009-09-30 01:09, Dan Doel wrote:
> Another suggestion I've seen is to restrict universe polymorphism to a rank-1 
> Hindley-Milner sort of discipline, and is that not good enough for this case?
> 
>   Substitutive : ∀ {a p} {A : Set a} → (A → A → Set a) → Set (p + 1)
>   Substitutive {a} {p} {A} _∼_
>       = (P : A → Set p) {x y : A} → x ∼ y → P x → P y
> 
>   subst : ∀{p} → Substitutive {a} {p} {A} _∼_
> 
> I guess it means that you'll have to do extra re-quantifying over levels, but 
> that may not be such a big deal in practice.

I prefer systems where, everything else being equal, I can abstract over
as much as possible. I guess everything else may not be equal in this
case, though.

-- 
/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.