module MagicWith where data _×_ (A : Set)(B : A -> Set) : Set where _,_ : (x : A) -> B x -> A × B fst : {A : Set}{B : A -> Set} -> A × B -> A fst (x , y) = x snd : {A : Set}{B : A -> Set}(p : A × B) -> B (fst p) snd (x , y) = y data Nat : Set where zero : Nat suc : Nat -> Nat record True : Set where data False : Set where IsZero : Nat -> Set IsZero zero = True IsZero (suc _) = False Uncurry : {A : Set}{B : A -> Set} -> ((x : A) -> B x -> Set) -> A × B -> Set Uncurry F p = F (fst p) (snd p) F : (n : Nat) -> IsZero n -> Set F zero _ = True F (suc _) () -- Trying to match only on fst p doesn't work since we can't abstract -- fst p without also abstracting snd p. f : (p : Nat × IsZero) -> Uncurry F p f p with fst p f p | zero = _ f p | suc _ = ?