{-# OPTIONS --cubical-compatible #-}

module Terra.Data.Nat where
open import Agda.Builtin.Nat using (Nat;suc;zero) public

-- private
--   variable
--     ℓ : Level

-- data Nat : Set where
--   zero : Nat
--   suc : Nat -> Nat

-- {-# BUILTIN NATURAL Nat #-}

data _≤_ : Nat -> Nat -> Set where
  orefl : {n : Nat} -> n ≤ n
  osuc : {a b : Nat} -> a ≤ b -> a ≤ suc b

_<_ : Nat -> Nat -> Set
l < r = suc l ≤ r

module _ where private
  v : Nat
  v =