MagicWith.agda

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 _ = ?