actuallygood.agda

data _⊔_is_ : ℕ → ℕ → ℕ → Set where
  m≥⊔nism : {m n : ℕ}
    → n ≤ m
      ---------
    → m ⊔ n is m

  m≤⊔nisn : {m n : ℕ}
    → m ≤ n
      ---------
    → m ⊔ n is n

data Total (m n : ℕ) : Set where
  forward : m ≤ n → Total m n
  flipped : n ≤ m → Total m n

≤total : (m n : ℕ) → Total m n
≤total zero n = forward z≤n
≤total (suc m) zero = flipped z≤n
≤total (suc m) (suc n) with ≤total m n
...                       | forward m≤n = forward (s≤s m≤n)
...                       | flipped n≤m = flipped (s≤s n≤m)

_⊔_ : (m n : ℕ) → Σ[ p ∈ ℕ ] (m ⊔ n is p)
m ⊔ n with ≤total m n
...      | forward m≤n = ⟨ n , m≤⊔nisn m≤n ⟩
...      | flipped n≤m = ⟨ m , m≥⊔nism n≤m ⟩