module sigmaset where

data Σ  (A : Set) (B : A -> Set)  : Set where
   p : (a : A) -> B a -> Σ A B


postulate A : Set
postulate B : A -> Set
postulate C : Set

f : Σ A B -> C
f (p a b) = {! !}