```agda
postulate
  _<?_ : ∀ (m n : ℕ) → Dec (m < n)
```

¬z<z : ¬ (zero < zero)
¬z<z ()
¬s<z : ∀ {m : ℕ} → ¬ (suc m < zero)
¬s<z ()
¬s<s : ∀ {m n : ℕ} → ¬ (m < n) → ¬ (suc m < suc n)
¬s<s ¬m<n (s<s m<n) = ¬m<n m<n
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
zero <? zero = no ¬z<z
zero <? suc n = yes z<s
suc m <? zero = no ¬s<z
suc m <? suc n with m <? n
...               | yes m<n = yes (s<s m<n)
...               | no ¬m<n = no (¬s<s ¬m<n)

```agda
postulate
  _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
```

open Eq using (sym; cong)
zero≢suc : {n : ℕ} → ¬ zero ≡ suc n
zero≢suc = λ()
≢-sym : ∀ {m n : ℕ} → ¬ n ≡ m → ¬ m ≡ n
≢-sym ¬n≡m m≡n = ¬n≡m (sym m≡n)
s≡s : ∀ {m n : ℕ} → suc m ≡ suc n → m ≡ n
s≡s refl = refl
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero ≡ℕ? zero = yes refl
zero ≡ℕ? suc n = no zero≢suc
suc m ≡ℕ? zero = no (≢-sym zero≢suc)
suc m ≡ℕ? suc n with m ≡ℕ? n
...                | yes m≡n = yes (cong suc m≡n)
...                | no m≢n = no λ suc-m≡suc-n → m≢n (s≡s suc-m≡suc-n)

postulate
  ∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
  ∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
  not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋

∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (yes _) (yes _) = refl
∧-× (yes _) (no _)  = refl
∧-× (no _)  (yes _) = refl
∧-× (no _)  (no _)  = refl
∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-⊎ (yes _) (yes _) = refl
∨-⊎ (yes _) (no _)  = refl
∨-⊎ (no _)  (yes _) = refl
∨-⊎ (no _)  (no _)  = refl
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ (yes _) = refl
not-¬ (no _)  = refl

```agda
postulate
  _iff_ : Bool → Bool → Bool
  _⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
  iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
```

_iff_ : Bool → Bool → Bool
true iff true = true
false iff false = true
_ iff _ = false
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
yes a ⇔-dec yes b = yes record { to = λ _ → b ; from = λ _ → a }
yes a ⇔-dec no ¬b = no λ a⇔b → ¬b ((_⇔_.to a⇔b) a)
no ¬a ⇔-dec yes b = no λ a⇔b → ¬a ((_⇔_.from a⇔b) b)
no ¬a ⇔-dec no ¬b = yes (record { to = λ a → ⊥-elim (¬a a) ; from = λ b → ⊥-elim (¬b b) })
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ (yes a) (yes b) = refl
iff-⇔ (yes a) (no ¬b) = refl
iff-⇔ (no ¬a) (yes b) = refl
iff-⇔ (no ¬a) (no ¬b) = refl

```agda
False : ∀ {Q} → Dec (¬ Q) → Set
False Q = T (not ⌊ Q ⌋)
toWitnessFalse : ∀ {A : Set} {D : Dec A} → T (not ⌊ D ⌋) → ¬ A
toWitnessFalse {D = no ¬a} tt = ¬a
fromWitnessFalse : ∀ {A : Set} {D : Dec A} → ¬ A → T (not ⌊ D ⌋)
fromWitnessFalse {D = yes a} ¬a = ¬a a
fromWitnessFalse {D = no ¬a} ¬a = tt
```

```agda
open import plfa.part1.Relations using (Bin; ⟨⟩; _I; _O)
open import plfa.part1.Quantifiers using (One; one; one-O; one-I; Can)
One? : ∀ (b : Bin) → Dec (One b)
One? ⟨⟩ = no λ()
One? (⟨⟩ I) = yes one
One? (b O) with One? b
...           | yes o = yes (one-O o)
...           | no ¬o = no λ {(one-O o) → ¬o o}
One? ((b O) I) with One? (b O)
...           | yes o = yes (one-I o)
...           | no ¬o = no λ {(one-I o) → ¬o o}
One? ((b I) I) with One? (b I)
...           | yes o = yes (one-I o)
...           | no ¬o = no λ {(one-I o) → ¬o o}

Can? : ∀ (b : Bin) → Dec (Can b)
Can? (⟨⟩ O) = yes Can.zero-bin
Can? ⟨⟩ with One? ⟨⟩
...        | no ¬o = no λ {(Can.leading o) → ¬o o}
Can? (b I) with One? (b I)
...           | yes o = yes (Can.leading o)
...           | no ¬o = no λ {(Can.leading o) → ¬o o}
Can? ((b O) O) with One? (b O)
...               | yes o = yes (Can.leading (one-O o))
...               | no ¬o = no λ {(Can.leading (one-O o)) → ¬o o}
Can? ((b I) O) with One? (b I)
...               | yes o = yes (Can.leading (one-O o))
...               | no ¬o = no λ {(Can.leading (one-O o)) → ¬o o}
```