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

[Nils Anders Danielsson]

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