{-# OPTIONS  --without-K #-}
module SizedNat where

open import Agda.Builtin.Equality
open import Agda.Builtin.Size

Size≤_ : Size → Set
Size≤ i = Size< (↑ i)

----------------------------------------------------------------------
-- Size-parameterized Nat
----------------------------------------------------------------------
data Nat (i : Size) : Set where
  zero : Nat i
  succ : (j : Size< i) → Nat j → Nat i

-- If j ≤ i, then Nat j is a subtype of Nat i
φ : (i : Size){j : Size≤ i} → Nat j → Nat i
φ _ x = x

-- The example from section 2 of the the Abel-Vezzosi-Winterhalter paper
pred : (i : Size) → Nat i → Nat i
pred _ zero       = zero
pred _ (succ _ x) = x

monus : (i : Size)(x : Nat i)(j : Size)(y : Nat j) → Nat i
monus _ x _ zero       = x
monus _ x _ (succ _ y) = monus _ (pred _ x) _ y

monus-diag : (i : Size)(x : Nat i) → zero ≡ monus i x i x
monus-diag i = m i
  where
  m : (j : Size≤ i)(x : Nat j) → zero ≡ monus i x j x
  m _ zero       = refl
  m _ (succ k x) = m k x

----------------------------------------------------------------------
-- Sized-indexed Nat
----------------------------------------------------------------------
data Nat' : (i : Size) → Set where
  zero : (i : Size) → Nat' (↑ i)
  succ : (i : Size) → Nat' i → Nat' (↑ i)

-- Now Nat' j is only a subtype of Nat i for j < i
φ' : (i : Size){j : Size< i} → Nat' j → Nat' i
φ' _ x = x
-- but not for j ≤ i !!
φ'' : (i : Size){j : Size≤ i} → Nat' j → Nat' i
φ'' _ x = {!!}

pred' : (i : Size) → Nat' i → Nat' i
pred' _ (zero i)   = zero i
pred' _ (succ _ x) = x

monus' : (i : Size)(x : Nat' i)(j : Size)(y : Nat' j) → Nat' i
monus' _ x _ (zero j)   = x
monus' _ x _ (succ _ y) = monus' _ (pred' _ x) _ y

-- Now we are blocked from completing the proof of zero ≡ monus x x
monus-diag' : (i : Size)(x : Nat' i) → zero i ≡ monus' (↑ i) x (↑ i) x
monus-diag' .(↑ i) (zero i)   = {!!}
monus-diag' .(↑ i) (succ i x) = {!!}