Bikeshedding #1326: what to do about _⇒_ and ∀[_] on SizedType

[andreasabel]

One proposal in continuation of #1326: remove _⇒_ and ∀[_] on SizedType

See discussion around #1326 (comment).

The nested module is not in style with the std-lib, and exporting these short definitions on top-level creates unpleasant clashes with Relation.Unary.

Thus, one solution is to remove the offending definitions and wait whether they will grow back naturally.

@MatthewDaggitt suggested instead:

I think a better solution is to mimic the normal module hierarchy underneath Size just as we do elsewhere in the library. For example we would put ∀[_] in Size.Relation.Unary and _⇒_ in Size.Function. That would make it so much easier to expand these later on if we found it necessary.

[gallais]

we would put ∀[_] in Size.Relation.Unary and ⇒ in Size.Function

I think both of them would go Size.Relation.Unary just like both of
their counterparts are in Relation.Unary.

[MatthewDaggitt]

I think both of them would go Size.Relation.Unary just like both of
their counterparts are in Relation.Unary.

Hmm except that ⇒ is not the counterpart of ⇒ in Relation.Unary right? It's just a "function" over sized types whereas _⇒_ in Sized.Relation.Unary should be a function over predicates over sized types. Hence why in #1326 I suggested a different arrow → for @andreasabel's definition here.

I'm not even sure what a "sized predicate" definition would look like. Something like?

Pred : ∀ {a} → SizedType a → (ℓ : Level) → SizedType (a ⊔ suc ℓ)
Pred A ℓ i = A i → Set ℓ

_⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ⇒ Q = λ x i → P (x i) → Q (x i)

Although now I think about it, isn't all this just a special case of Relation.Unary.Indexed with I = Size?

[gallais]

It literally is a replacement for Relation.Unary combinators that
cannot be used anymore because Size is not a Set anymore in
the dev version of Agda.

[MatthewDaggitt]

It literally is a replacement for Relation.Unary combinators that
cannot be used anymore because Size is not a Set anymore in
the dev version of Agda.

Hmm yes, you're right. I'm getting confused somewhere. Thanks for bearing with me and pointing that out. Okay I'm happy for them to go in Size.Relation.Unary then 😄

[MatthewDaggitt]

I've implemented the discussed change. The one difference was that I've moved it to Relation.Unary.Sized rather than Size.Relation.Unary. Couple of reasons:

1. I was thinking where would be put sized naturals if we wanted to add them. We'd definitely add them under Data.Nat.Sized rather than Size.Data.Nat right?
2. We already have things like Relation.Unary.Indexed.

[gallais]

Should SizedType be SizedSet? 👼

[andreasabel]

Should SizedType be SizedSet? 👼

Maybe, but isn't the long term plan for Agda to move from Set to Type?

[jespercockx]

Maybe, but isn't the long term plan for Agda to move from Set to Type?

By the time we get to version 3 maybe?

[MatthewDaggitt]

Let's stay consistent with the current version of Agda. When and if Agda 3 rolls around, I'm sure deprecating SizedSet for SizedType will be the least of our worries!