T? : ∀ x → Dec (T x)
¬? : Dec A → Dec (¬ A)
⊤-dec : Dec {a} ⊤
_×-dec_ : Dec A → Dec B → Dec (A × B)
⊥-dec : Dec {a} ⊥
_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
_→-dec_ : Dec A → Dec B → Dec (A → B)

------------------------------------------------------------------------
-- Interaction with negation, sum, product etc.

infixr 1 _⊎?_
infixr 2 _×?_ _→?_

T? : ∀ x → Dec (T x)
T? x = x because T-reflects x

¬? : Dec A → Dec (¬ A)
does  (¬? a?) = not (does a?)
proof (¬? a?) = ¬-reflects (proof a?)

⊤? : Dec {a} ⊤
does  ⊤? = true
proof ⊤? = ⊤-reflects

_×?_ : Dec A → Dec B → Dec (A × B)
does  (a? ×? b?) = does a? ∧ does b?
proof (a? ×? b?) = proof a? ×-reflects proof b?

⊥? : Dec {a} ⊥
does  ⊥?  = false
proof ⊥?  = ⊥-reflects

_⊎?_ : Dec A → Dec B → Dec (A ⊎ B)
does  (a? ⊎? b?) = does a? ∨ does b?
proof (a? ⊎? b?) = proof a? ⊎-reflects proof b?

_→?_ : Dec A → Dec B → Dec (A → B)
does  (a? →? b?) = not (does a?) ∨ does b?
proof (a? →? b?) = proof a? →-reflects proof b?