Convert an uncurried function on
Sigma to a curried one.
Together,
currySigma and
uncurrySigma witness an
isomorphism such that the following identities hold:
id1 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
(forall (p :: Sigma a b). SSigma p -> c @ p)
-> (forall (p :: Sigma a b). SSigma p -> c p)
id1 f = uncurrySigma a b c (currySigma a b c f)
id2 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
(forall (x :: a) (sx :: Sing x) (y :: b x). Sing (WrapSing sx) -> Sing y -> c (sx :&: y))
-> (forall (x :: a) (sx :: Sing x) (y :: b x). Sing (WrapSing sx) -> Sing y -> c (sx :&: y))
id2 f = currySigma a b c (uncurrySigma a b @c f)