module symnat where


data ℕ : Set where
  Z : ℕ 
  S : ℕ -> ℕ 


data Bool : Set where
  tt : Bool
  ff : Bool

data ⊤ : Set where
  true : ⊤ 

data ⊥ : Set where


Atom : Bool -> Set
Atom tt = ⊤ 
Atom ff = ⊥ 

_==Bool_ : ℕ -> ℕ -> Bool
Z     ==Bool  Z     = tt
(S n) ==Bool  (S m) = n ==Bool m
_     ==Bool  _     = ff


_==_ : ℕ -> ℕ -> Set
n == m = Atom ( n ==Bool m)


Sym : Set
Sym = (n m : ℕ) -> n == m -> m == n


sym : Sym
sym Z     Z     _  = true
sym Z     (S m) ()
sym (S n) Z     ()  
sym (S n) (S m) nm = sym n m nm