[Agda] Setω and abstraction

[Nils Anders Danielsson]

Hi,

The following code does not type check because "Setω is not a valid
type":

  Substitutive : ∀ {a} {A : Set a} → (A → A → Set a) → ?
  Substitutive {A = A} _∼_ =
    {p : Level} (P : A → Set p) {x y : A} → x ∼ y → P x → P y

This definition states that a relation _∼_ (in a certain universe) is
substitutive if /all/ relevant predicates (in arbitrary universes)
respect the relation.

I can see that the type of this definition is problematic; in order to
type code of the form

  ∀ {ℓ : Level} → …

there has to be a "level" which is not an inhabitant of Level. However,
the body of Substitutive is valid code:

  postulate
    subst : {p : Level} (P : A → Set p) {x y : A} → x ∼ y → P x → P y

This points to a problem: I can write down the type signature of subst,
but I cannot give the type a name. Are there any thoughts about this?

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