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

[Daniel Peebles]

Hi Nils,

Thanks for this. I just used a lowercase letter for Pred because
that's what was already there. I'll take note of your points about
conventions though, and will try to conform to them!

As the new Pred you suggest introduces a new argument, would it not be
better to go with the REL/Rel distinction and make a PRED/Pred pair,
for backwards compatibility? Or is the REL/Rel pair just a stopgap
measure?

I'll experiment with your suggestions and see where they take me.

Thanks,
Dan

On Fri, Dec 11, 2009 at 6: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.
>
> --
> /NAD
>
>