[Agda] partial division property

[Nils Anders Danielsson]

On 2012-11-04 18:09, Serge D. Mechveliani wrote:
>    (a : A) -> (b : A) -> case divMb a b of н╩
>                          { (just q) -> (q * b) \~~ a
>                          ; nothing  -> (x : A) -> \neg ((x * b) \~~ a)
>                          }

I think your problem is that the two branches above have different
universe levels. You can use lifting (Level.Lift) to coerce one or both
branches to a common universe level.

-- 
/NAD