open import Paths
open import Logic::HLevels
open import Algebra::Formula

open data FMSet (A : Type)
| nil
| infixr :< A (FMSet A) tighter =
| comm (x y : A) (xs : FMSet A) : x :< y :< xs = y :< x :< xs
| trunc : isSet (FMSet A)

variable A : Type

def infixr ++ : BinOp (FMSet A)
| nil, ys ⇒ ys
| x :< xs, ys ⇒ x :< xs ++ ys
| comm x y xs i, ys ⇒ comm x y (xs ++ ys) i
| trunc xs zs p q i j, ys ⇒
  trunc (xs ++ ys) (zs ++ ys) (pmap (++ ys) p) (pmap (++ ys) q) i j
tighter :< =