MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "SgPredWrongMon.ma" ---
--- scope checking ---
--- type checking ---
univ  Pred : - Set -> Set 1
univ  Pred = \ A -> A -> Set
type  Sg : ++(A : Set) -> ^ A -> Set
term  Sg.sg : .[A : Set] -> .[elem : A] -> < Sg.sg elem : Sg A elem >
type  Nat : + Size -> Set
term  Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze
term  Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i >
type  Sg' : +(A : Set) -> A -> Set
type  Sg' = Sg
--- evaluating ---
--- closing "SgPredWrongMon.ma" ---