module Data.Alphabet

import Control.SUSY
import Control.Total
import Data.SUSY

export
(Super a, Super b) => Super (a,b) where
    deg (x, y) = deg x + deg y

export
[SL] (Letter a, Ord b) => Ord (a,b) where
    compare (x, xx) (y, yy) with (compare x y)
      _ | EQ with (deg x)
          _ | Boson = compare xx yy
          _ | Fermion = contra $ compare xx yy
      _ | t = t

(Letter a, AntiSym b) => AntiSym (a,b) using SL where
    antisym (x, xx) (y, yy) with (compare x y) proof p
      _ | LT = rewrite antisym y x in rewrite p in Refl
      _ | EQ with (deg x) proof pp
        _ | Boson = rewrite antisym y x in rewrite p in rewrite sym $ degeq x y {p=p} in rewrite pp in antisym xx yy
        _ | Fermion = rewrite antisym y x in rewrite p in rewrite sym $ degeq x y {p=p} in rewrite pp in rewrite antisym xx yy in Refl
      _ | GT = rewrite antisym y x in rewrite p in Refl