SizeSucMonotone.agda

-- Andreas, 2012-09-24 Ensure that size successor is monotone
{-# OPTIONS --sized-types #-}
module SizeSucMonotone where

open import Common.Size

postulate Size< : Size → Set
{-# BUILTIN SIZELT Size< #-}

data Bool : Set where
  true false : Bool

-- T should be monotone in its second arg
T : Bool → Size → Set
T true  i = Size< i
T false i = Size< (↑ i)

test : {x : Bool}{i : Size}{j : Size< i} → T x j → T x i
test h = h