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

[Luke Palmer]

On Fri, Dec 11, 2009 at 4:38 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> 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.

God forbid we should use multiple letters!

(A : Set ℓa)

Which doesn't interfere with the existing convention:

(a : A) -> ...

Luke