[Agda] fromJ ∘ toJ level

[Twan van Laarhoven]

map-compose proves the equality the other way around, so you need

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

or

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


Twan

On 15/10/13 14:24, Sergei Meshveliani wrote:
> 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}
> -------------------------------------------------------------------------
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>