Setoid for List composed n-times: second level is constrained to >= first level

[mechvel]

The impression is that it is not possible to set the level values below such that Agda would type check this program:

open import Data.List.Relation.Binary.Pointwise as ListPoint
open import Data.Nat using (ℕ; suc)
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)

module ComposeListSetoid {a ℓ} (S : Setoid a ℓ) where

-- Having Setoid  S  on Carrier, build Setoid for  List (List ... Carrier)  -- n-times.

composeSetoid : ℕ → Setoid _ _   -- a (a ⊔ ℓ)  ?
composeSetoid 0       = S
composeSetoid (suc n) = ListPoint.setoid S'
                        where
                        S' : Setoid _ _    -- a (a ⊔ ℓ) ?
                        S' = composeSetoid n

[andreasabel]

This is more an issue for the standard library.

It works if you assume S : Setoid a (a ⊔ ℓ) instead. Apparently the second level has to be at least as big as the first.

module _ {a ℓ} (S : Setoid a (a ⊔ ℓ)) where

-- Having Setoid  S  on Carrier, build Setoid for  List (List ... Carrier)  -- n-times.

composeSetoid : ℕ → Setoid a (a ⊔ ℓ)   -- a (a ⊔ ℓ)  ?
composeSetoid 0       = S
composeSetoid (suc n) = ListPoint.setoid S'
  where
  S' : Setoid a (a ⊔ ℓ)    -- a (a ⊔ ℓ) ?
  S' = composeSetoid n

[mechvel]

Thank you for explanation.
Now, when it is given (S : Setoid a ℓ),
is there a way to apply the above (composeSetoid n S) ?
To help this, I tried

lift : Setoid a ℓ → Setoid a (a ⊔ ℓ)                                            
lift S = S                                                                      

But it is rejected. Is there a way to lift a data to a higher level?

I am sorry if this is an issue for Standard library, I do not know.

In a real example, I use

CommutativeRing α α=,     -- of Standard library                                
DecCommutativeRing α α=   -- the condition of _≟_ added                         
Pol                       -- constructor of univariate polynomial               
module OverDecComRing {α α=} (R : DecCommutativeRing α α=)                      
  where ...                                                                     
polDecCommutativeRing :  DecCommutativeRing (α ⊔ α=) (α ⊔ α=)                   
...  

So, applying OverDecComRing n-times one has a sequence of instances of DecCommuitativeRing:

R  : DecCommmutativeRing α α=                                                   
R1 = OverDecComRing.polDecCommutativeRing R                                     
...                                                                             
Rn = OverDecComRing.polDecCommutativeRing R[n-1]                                

The first member has the level pair α α=, others probably need to have (α ⊔ α=) (α ⊔ α=).
Due to standard of CommutativeRing α α=
I cannot define another levels for DecCommmutativeRing.
And for polDecCommutativeRing, the pair (α ⊔ α=) (α ⊔ α=)
is the minimal possible, it is not possible to change.
Is it?

So, I fail to program computing Rn, because R0 = R differs in level.

I can program this for n ≢ 0, but this is not so nice, the domain R looks like a nicer base for recursion.
?

[andreasabel]

To help this, I tried

lift : Setoid a ℓ → Setoid a (a ⊔ ℓ)
lift S = S
But it is rejected. Is there a way to lift a data to a higher level?

Yes, but not just via subtyping (as you tried), but you have to use the Lift constructor, which works on Set, so you have to define liftSetoid by Lifting the types in Setoid.

[jamesmckinna]

Try: (UPDATED to typecheck as a free-standing fragment)

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S

  lift : ∀ a → Setoid c (a ⊔ ℓ)
  lift a = record
    { _≈_ = _≈↑_
    ; isEquivalence = record { refl = refl↑ ; sym = sym↑ ; trans = trans↑ }
    }
    where
    _≈↑_ : Rel Carrier (a ⊔ ℓ)
    x ≈↑ y = Level.Lift a (x ≈ y)
    refl↑ : Reflexive _≈↑_
    refl↑ = Level.lift refl
    sym↑ : Symmetric _≈↑_
    sym↑ (Level.lift x≈y) = Level.lift (sym x≈y)
    trans↑ : Transitive _≈↑_
    trans↑ (Level.lift x≈y) (Level.lift y≈z) = Level.lift (trans x≈y y≈z)

While @andreasabel is correct regarding the defined choice of Levels for bundles in stdlib, I do still regret that Agda's approach to level polymorphism for records makes this kind of heavyweight construction necessary... given that a record is a particular kind of parametrised Set, it's pity that Level-lifting for Set can't 'see through' the telescopic parametrisation associated to records.

But that may simply be magical thinking on my part (but, I suspect, also that of other users, esp. beginners when first encountering Levels...)

[mechvel]

Thanks to people for the explanation.
The code by James is not type-checked, for several reasons.
I modify it this way:

import      Data.List.Relation.Binary.Pointwise as ListPoint
open import Data.Nat using (ℕ; suc)
open import Level using (_⊔_)
open import Relation.Binary

liftSetoid : ∀ {a ℓ} → Setoid a ℓ → Setoid a (a ⊔ ℓ)     -- lifted is (S : Setoid _ _), not a level
liftSetoid {a} {ℓ} S = record
  { _≈_ = _≈↑_
  ; isEquivalence = record { refl = refl↑ ; sym = sym↑ ; trans = trans↑ }
  }
  where
  open Setoid S

  _≈↑_ : Rel Carrier (a ⊔ ℓ)
  x ≈↑ y = Level.Lift a (x ≈ y)

  refl↑ : Reflexive _≈↑_
  refl↑ = Level.lift refl

  sym↑ : Symmetric _≈↑_
  sym↑ (Level.lift x≈y) = Level.lift (sym x≈y)

  trans↑ : Transitive _≈↑_
  trans↑ (Level.lift x≈y) (Level.lift y≈z) = Level.lift (trans x≈y y≈z)

It is type checked. Did you mean this?
Usage in my initial example:

module Compose {a ℓ} (S : Setoid a ℓ)
  where
  -- Having Setoid  S  on Carrier,
  -- build Setoid for  List (List ... Carrier)  -- n-times.

  composeSetoid : ℕ → Setoid a (a ⊔ ℓ)
  composeSetoid 0       = liftSetoid S
  composeSetoid (suc n) = ListPoint.setoid S'
       where
        S' : Setoid a (a ⊔ ℓ)
        S' = composeSetoid n

But in reality people will need to lift standard structures like
Magma, Semigroup, ..., CommutativeRing ... --- may be dowzens of them.
They will also need to lift structures in their applied programs:
DecCommutativeRing; DecIntegralDomain, GCdSemiring, GCDDomain ...
Currently I need to program

composeDecCommutativeRing :
  ∀ {a ℓ} (R : DecCommutativeRing a ℓ) → ℕ → DecCommutativeRing _ _
composeDecCommutativeRing R 0 =  R
composeDecCommutativeRing R (suc n) =
  OfPolynomial.OverDecComRing.polDecCommutativeRing
      (composeDecCommutativeRing R n)
  -- applying a function from the parametric package for Polynomial

How simple is it to lift, say, CommutativeRing ?

Currently, I use the format

composeDecCommutativeRing :  ∀ {a ℓ} (R : DecCommutativeRing a (a ⊔ ℓ) → ℕ →
                                                            DecCommutativeRing a (a ⊔ ℓ),

which avoids lifting. And it works in the example of R = DecCommutativeRing-for-Integer.
In this case, the call

  composeDecCommutativeRing DecCommutativeRing-for-Integer n

is type-checked, because a = ℓ = 0.
But in more general examples, a programmer will have R : DecCommutativeRing a ℓ,
and the above format for composeDecCommutativeRing will not fit.
Changing a format to a regular one will need lifting of DecCommutativeRing, which is probably a messy work (is it?).

The whole subject looks strange, I do not understand of whether it has an easy solution in general.
Is lifting really needed on practice? If yes, then how to apply it to records?

[andreasabel]

Using Setoid a (a ⊔ ℓ) instead of Setoid a ℓ restricts uses to situation where the type of the equality relation is at least as big as the type of the carrier.
I don't know if in practice this is a real restriction, because I do not have an example suite in my head.

[jamesmckinna]

Apologies for sloppy editing above. I have now corrected the code fragment. Hopefully this will now typecheck for @mechvel , but as @andreasabel points out, the choices may be suboptimal wrt lifting being 'fully' Level-polymorphic. Nevertheless, I presume(d) that it is sufficient for the purposes at hand...
... as for extensions also to other algebraic structures, that's why I opened issue #2767 to track this specific use case. As for iterating List in order to consider polynomial extension of a ring in many variables, I guess that's one way to represent that construction. Certainly we don't (yet) have systematic development of free algebras and free extensions in stdlib, but I hope that situation will change in future releases... cf. #1962 and various other issues/PRs which touch on the possible design space.

[mechvel]

Andreas wrote

Using Setoid a (a ⊔ ℓ) instead of Setoid a ℓ restricts uses to situation where the type of the equality relation is at least as b

Andreas wrote

Using Setoid a (a ⊔ ℓ) instead of Setoid a ℓ restricts uses to situation where the type of the equality relation is at least as > big as the type of the carrier.
I don't know if in practice this is a real restriction, because I do not have an example suite in my head.

Probably there are possible only this kind of setoids.
We have
(1) the Setoid record arguments are named a and ℓ in its definition,
(2) any data S : Setoid a ℓ must belong to Setoid a (a ⊔ ℓ)
?

Explanation for (2).
According to the classical axiomatic set theory (of which I know quite few)
a binary relation ~ on Carrier (: Set a) is a subset of Carrier × Carrier.
In the case of Setoid, ≈ is reflexive, so that all the pairs (x,x) for x : Carrier
belong to ≈. So ≈ includes an injective image of Carrier,
so that level(≈) has to be ≥ a, and it is equivalent to (a ⊔ ℓ).

I doubt about fitness of the classical set-theoretical discourse here.
On the other hand, I feel that if Carrier : Set a, and ~ is a reflexive relation on Carrier,
then level(~) is at least (a ⊔ ℓ) in any case.

And in my program there are declared

record DecCommutativeRing α α≈ :  Set (sucL (α ⊔ α≈))                           
  ...                                                                           
  field  commutativeRing : CommutativeRing α α≈                                 
  ...                                                                           

Further:

module Pol.OverDecComRing {α α=} (R : DecCommutativeRing α α=) where
...
polDecCommutativeRing : DecCommutativeRing (α ⊔ α=) (α ⊔ α=)
polDecCommutativeRing = ...

On the other hand, R has a setoid inside it. So, if Carrier(R) : Set α,
then R must belong at least to DecCommutativeRing α (α ⊔ α=).

Still, I can use the composition of
Pol.OverDecComRing.polDecCommutativeRing n-times, only with setting compose to have the arguments
(n : ℕ) → (R : DecCommutativeRing (α ⊔ α=) (α ⊔ α=)).

Ant it may occur that the suggestion of Andreas is sufficient
(Lift is not necessary here, and changes in Standard library are not necessary here).
But I am not sure.
Let us see the further experience and possible opinions.

[mechvel]

James wrote
"... as for extensions also to other algebraic structures, that's why I opened issue #2767 to track this specific use case. As for iterating List in order to consider polynomial extension of a ring in many variables, I guess that's one way to represent that construction. Certainly we don't (yet) have systematic development of free algebras and free extensions in stdlib, but I hope that situation will change in future releases... cf. #1962 and various other issues/PRs which touch on the possible design space."

It is not natural for Standard library of Agda to include various models of polynomial algebra, free algebras, Lie algebras, and so on. This is a matter of applied libraries.
Do not include all algebra (nor all mathematics) into Standard library for a language.

I mentioned an example of using the Pol constructor for polynomials (record ... Pol where ....) in my applied program because I had a certain small problem with its recursive application.
Andreas has advised on setting the level expressions, and this looks sufficient.
But it needs further experience.
Also there arose aside the question of lifting records.
I doubt of whether it is critical for my current experience with Pol, but generally this question has sense
(is it really needed? If yes, than how to arrange lifting records).