I'm trying to prove that type-level function Union is associative, but I'm not sure how it should be done. I proved right identity and associativity laws for type-level append function and right identity for union:
data SList (i :: [k]) where
SNil :: SList '[]
SSucc :: SList t -> SList (h ': t)
appRightId :: SList xs -> xs :~: (xs :++ '[])
appRightId SNil = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl
appAssoc
:: SList xs
-> Proxy ys
-> Proxy zs
-> (xs :++ (ys :++ zs)) :~: ((xs :++ ys) :++ zs)
appAssoc SNil _ _ = Refl
appAssoc (SSucc xs) ys zs = case appAssoc xs ys zs of Refl -> Refl
cong :: a :~: b -> f a :~: f b
cong Refl = Refl
unionRightId :: SList xs -> AsSet xs :~: Union xs '[]
unionRightId xs = case cong (appRightId xs) of Refl -> Refl
but I don't get how to prove that union is associative.
Sort
is a sort.) For a complex proof like this, that seems like an absolutely critical first step. – Prendergast