natU : ℕ → UnatU 0 ≔ ⊤natU _ = ⊥th : 0 = 1 → Void -- aka 0 ≠ 1th prf = (tr (ap natU prf)) ★-- ⊤ = ⊥ -- ⊤ → ⊥ -- ⊥