e' : Nat -> Nat -> Ordering
e' i j = 

-- U_q(\mathcal{g}) q->0 limit
-- idk about superalgebra case
--todo: prove braiding relation
--todo: prove that we change i -> i+1
paren : Nat -> Nat -> Ordering
paren i j = 

f' : Nat -> Nat -> Ordering
f' i = contra . e' i
scan : Ordering -> Nat -> Maybe Nat
scan LT Z = Nothing
scan LT (S x) = Just x
scan EQ x = Just $ x
scan GT x = Just $ S $ x

(+) : Ordering -> Nat -> Maybe Nat
LT + Z = Nothing
LT + (S x) = Just x
EQ + x = Just $ x
GT + x = Just $ S $ x

scanner : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)
scanner (x, y) (w, z) with (scan w y)

scan : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)
scan (x, y) (w, z) with (w + y)

fi : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n
fi a = fst $ foldl scanner (Nothing, Z) $ zip a $ allFins n

argmin : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n
argmin a = fst $ foldl scan (Nothing, Z) $ zip a $ allFins n

e i x = pure $ replaceAt (complement !(fi $ e' i <$> reverse x)) i x

e i x = pure $ replaceAt (complement !(argmin $ paren i <$> reverse x)) i x

f i x = pure $ replaceAt !(fi $ f' i <$> x) (S i) x

f i x = pure $ replaceAt !(argmin $ (contra . paren i) <$> x) (S i) x