[Agda] fromJ ∘ toJ level

[Sergei Meshveliani]

People,

I have
1) C =  Carrier,
2) J =  subset of just-s in  Maybe C,
3) toJ : C -> J,  fromJ : J -> C   
                  -- mutually inverse maps defined as shown below, 

and need to prove   (map fromJ ∘ map toJ) ≗ map (fromJ ∘ toJ). 
The proof             
            map-compose {A = C} {B = J} {C = C}

uses  Data.List.Properties.map-compose.

First, I have tested  map-compose  on   
                                   g = proj₁,  f = \x -> (x , x),
and it works.
Also                        fromJ ∘ toJ ≗ id   
is proved by  PropEq.refl.

But for  fromJ -- toJ,  the checker reports 

  Set α != Set (sucL α= ⊔ sucL α);
  when checking that the expression
  map-compose {A = C} {B = J} {C = C} has type
  (λ {.x} → map fromJ) ∘ map toJ ≗ map ((λ {.x} → fromJ) ∘ toJ)

May this be due to some level mismatch? 
toJ  maps to a level that may be higher than  α
(because the  Subset  data over  Maybe C  may have a higher level than
C). 
But  fromJ  returns from this higher level to  C.
So, I wonder.
I tried inserting  lower, lift, Lift  in various places, and failed.

Thank you in advance for hint,

------
Sergei



----------------------------------------------------------------------
module Maybe-DSet-pack (α α= : Level) (upDS : UpDSet α α=)
  where
  dSet = UpDSet.dSet upDS
  open DSet dSet using    (setoid; decSetoid; _≈_; isEquivalence)
                 renaming (Carrier to C)

  eDecSetoid = Mb.decSetoid decSetoid
  open DecSetoid eDecSetoid using ()
               renaming (Carrier to eC; setoid to eSetoid; _≈_ to _=e_)

  isJust : eC → Set 0ℓ
  isJust = T ∘ maybeToBool

  congIsJust : isJust Respects _=e_
  congIsJust = ...

  memJ-struct : CongMember eSetoid
  memJ-struct = congMember isJust congIsJust

  J : Set (subcarrierLevel α α= 0ℓ)
  J = Subset eSetoid memJ-struct    -- set of just-s 

  toJ : C → J
  toJ x = subEl (just x) _

  fromJ : J → C
  fromJ (subEl (just x) _) = x
  fromJ (subEl nothing ())

  fromJ∘toJ=id :  fromJ ∘ toJ ≗ id
  fromJ∘toJ=id _ =  ≡refl

  mapFromJ∘mapToJ :  (map fromJ ∘ map toJ) ≗ map (fromJ ∘ toJ)
  mapFromJ∘mapToJ =  map-compose {A = C} {B = J} {C = C}
-------------------------------------------------------------------------