# [Agda] fromJ ∘ toJ level

Sergei Meshveliani mechvel at botik.ru
Tue Oct 15 15:24:37 CEST 2013

```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}
-------------------------------------------------------------------------

```