Documentation

leftId :: forall {k} p (x :: Ctx k). p x -> ((EmptyCtx :: Ctx k) <+> x) :~: x Source #

assoc :: forall {k} p (x :: Ctx k) q (y :: Ctx k) r (z :: Ctx k). p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z) Source #