[Agda] Setω and abstraction

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Wed Sep 30 12:00:50 CEST 2009

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.


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.

More information about the Agda mailing list