[Agda] Converting Relation.Unary to be universe-polymorphic

[Nicolas Pouillard]

Excerpts from Nils Anders Danielsson's message of Fri Dec 11 12:38:44 +0100 2009:
> On 2009-12-11 02:57, Daniel Peebles wrote:
> > Anyway, Relation.Unary's main function is, with universe polymorphism:
> >
> > Pred : ∀ {ℓ} → Set ℓ → Set (suc ℓ)
> > Pred {ℓ} a = a → Set ℓ
> 
> I don't think this definition is general enough. For homogeneous binary
> relations I currently use the following definition:
> 
> REL : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
> REL A ℓ = A → A → Set ℓ
> 
> > [...] I run into the issue of needing a universe-polymorphic ⊥.
> 
> I don't think we should make non-parametrised types
> universe-polymorphic. You would not get this problem if you defined Pred
> as follows:
> 
>   Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
>   Pred A ℓ = A → Set ℓ
> 
> > The other major problem in Relation.Unary I have is with the _⟨⊎⟩_
> > operator at the bottom of the module. Fully universe-polymorphic, its
> > type is (I think):
> >
> > ∀ {ℓA ℓB : Level} {A : Set ℓA} {B : Set ℓB} → Pred A → Pred B → Pred (A ⊎ B)
> >
> > But if I maintain the original definition, applying either one of the
> > input predicates gives me a Set either in ℓA or ℓB, and the return
> > type is in ℓA ⊔ ℓB, and agda can't unify those two.
> 
> With my suggested definition of Pred you have at least two options here.
> One is to turn _⟨⊎⟩_ into a data type, and the other is to define a
> function which computes the resulting level (see Data.Vec.N-ary.Eq).
> 
> By the way, if you are modifying the standard library it would be nice
> if you could follow the conventions which are currently used. Names of
> sets are usually capitalised (except in old code), and the corresponding
> levels use the corresponding lower-case letter (A : Set a). The letter ℓ
> is used for levels without a corresponding named set.

However this convention conflicts with naming 'a' an element of type 'A',
it makes sense as well.

Note that, I don't want to oppose myself on a fixed convention at all.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr