data Bool : Set where
  true : Bool
  false : Bool

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A

data _==_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x == x

sameNat : {a b : Bool} -> Maybe (a == b)
sameNat = just refl
sameNat = nothing

{-
.a != .b of type Bool
-}