{-# OPTIONS --safe #-}

module DepthComonads.Nat where

open import Agda.Builtin.Nat
  using (zero; suc; _+_)
  renaming (Nat to ℕ; _<_ to _<ℕᴮ_)
  public
open import DepthComonads.Bool
open import DepthComonads.Level

_<ℕ_ : ℕ → ℕ → Type
n <ℕ m = T (n <ℕᴮ m)