MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "BoxNeg.ma" ---
--- scope checking ---
--- type checking ---
type  Box : ^(A : Set) -> Set
term  Box.box : .[A : Set] -> ^(y0 : A) -> < Box.box y0 : Box A >
type  Neg : Set
term  Neg.neg : ^(y0 : Box Neg -> Neg) -> < Neg.neg y0 : Neg >
error during typechecking:
checking positivity
/// polarity check ++ <= ^ failed