1
{-# OPTIONS --sized-types --show-implicit #-}
4
open import Common.Size
6
data Nat : {size : Size} -> Set where
7
zero : {size : Size} -> Nat {↑ size}
8
suc : {size : Size} -> Nat {size} -> Nat {↑ size}
12
A = (Id : {i : Size} -> Nat {_} -> Set)
13
(k : Size)(m : Nat {↑ k}) -> Id {k} m
15
(j : Size)(n : Nat {j}) -> Id {j} n