\begin{code} 

module decidable-and-discrete where

open import mini-library

decidable : Set  Set
decidable X = X + (X  )

discrete : Set  Set
discrete X = {x y : X}  decidable(x  y)

₂-discrete : discrete 
₂-discrete {} {} = in₀ refl
₂-discrete {} {} = in₁(λ())
₂-discrete {} {} = in₁(λ())
₂-discrete {} {} = in₀ refl

\end{code}