meme.agda

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ}
      -------
    → zero ≤ n

  s≤s : {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
  m≥⊔n≡m : {m n : ℕ}
    → n ≤ m
      ---------
    → m ⊔ n ≡ m

  m≤⊔n≡n : {m n : ℕ}
    → m ≤ n
      ---------
    → m ⊔ n ≡ n

infix 4 _≤_

data Formula : ℕ → Set where
  var : ∀{m} → (n : ℕ) → n ≤ m → Formula m
  ∩_ : ∀{m} → Formula m → Formula (suc m)
  ∪_ : ∀{m} → Formula m → Formula (suc m)
  α : ∀{m n p} → Formula m → Formula n → (m ⊔ n ≡ p) → Formula p
  ν : ∀{m n p} → Formula m → Formula n → (m ⊔ n ≡ p) → Formula p

x : Formula zero
x = var zero z≤n

∩xx : Formula (suc zero)
∩xx = ∩ (var zero z≤n)

xα∩xx : Formula (suc zero)
xα∩xx = α x ∩xx (m≤⊔n≡n z≤n)

∩xxαx : Formula (suc zero)
∩xxαx = α ∩xx x (m≥⊔n≡m z≤n)

∩xxα∩xx : Formula (suc zero)
∩xxα∩xx = α ∩xx ∩xx (m≥⊔n≡m (s≤s z≤n))