open import Size

data NatF (a : Set) : Set where
  zeroF : NatF a
  succF : a → NatF a

{-# NO_POSITIVITY_CHECK #-}
data μ {i : Size} (F : Set → Set) : Set where
  In : {j : Size< i} → F (μ {j} F) → μ {i} F

pred' : ∀ {i} → μ {i} NatF → μ {i} NatF
pred' (In zeroF) = In zeroF
pred' (In (succF x)) = {!cannot type check with x!}

data Nat {i : Size}  : Set where
  In : {j : Size< i} → NatF (Nat {j}) → Nat {i}

pred : ∀ {i} → Nat {i} → Nat {i}
pred (In zeroF) = In zeroF
pred (In (succF x)) = x