IrrHeterogeneousSize.golden

MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "IrrHeterogeneousSize.ma" ---
--- scope checking ---
--- type checking ---
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  good : .[Size] -> .[f : .[i : Size] -> Nat i -> Set] -> (g : .[i : Size] -> (n : Nat i) -> f [i] n) -> (h : f [#] (Nat.zero [#]) -> Set) -> Set
{ good [i] [f] g h = h (g [$i] (Nat.zero [i]))
}
--- evaluating ---
--- closing "IrrHeterogeneousSize.ma" ---