📕.agda

module 📕 where

open import Agda.Primitive
  renaming (Set to 💯; lsuc to 👆; lzero to 🔴; Level to 🏢)

data _🤝_ {🤣 : 🏢} {🇦 : 💯 🤣} (🇽 : 🇦) : 🇦 → 💯 🤣 where
  ✅ : 🇽 🤝 🇽

infix 4 _🤝_

data #⃣ : 💯 where
  0⃣ : #⃣
  🔝 : #⃣ → #⃣

_➕_ : #⃣ → #⃣ → #⃣
🔝 🇽 ➕ 🇾 = 🔝 (🇽 ➕ 🇾)
0⃣ ➕ 🇾 = 🇾

infixl 6 _➕_

1⃣ = 🔝 0⃣
2⃣ = 🔝 1⃣
3⃣ = 🔝 2⃣
4⃣ = 🔝 3⃣
5⃣ = 🔝 4⃣
6⃣ = 🔝 5⃣
7⃣ = 🔝 6⃣
8⃣ = 🔝 7⃣
9⃣ = 🔝 8⃣


😬 : 2⃣ ➕ 2⃣ 🤝 4⃣
😬 = ✅