Frankly everything you need to know about me should already be in the sidebar. Here, have some Agda instead:
{-# OPTIONS --sized-types #-}
open import Size
open import Data.Empty
data _<_ : Size → Size → Set where
lt : ∀ s → (r : Size< s) → r < s
data Acc (s : Size) : Set where
acc : (∀ {r} → r < s → Acc r) → Acc s
false₁ : ⊥
false₁ = ¬wf∞ (wf ∞) where
wf : ∀ s → Acc s
wf s = acc (λ {(lt .s r) → wf r})
¬wf∞ : Acc ∞ → ⊥
¬wf∞ (acc p) = ¬wf∞ (p (lt ∞ ∞))Oh? You want more? Here's more:
data _≡_ : Size → Size → Set where
refl : ∀ {i} → i ≡ i
data Up! : Size → Set where
huh : ∀ {i} → Up! i
up! : ∀ {i} → {j : Size< i} → Up! j → Up! i
false₂ : ⊥
false₂ = hup! ∞ refl huh where
hup! : ∀ i → i ≡ (↑ ∞) → Up! i → ⊥
hup! .∞ refl u = hup! ∞ refl (up! u)