4
data _×_ (A : Set)(B : A -> Set) : Set where
5
_,_ : (x : A) -> B x -> A × B
7
fst : {A : Set}{B : A -> Set} -> A × B -> A
10
snd : {A : Set}{B : A -> Set}(p : A × B) -> B (fst p)
17
record True : Set where
18
data False : Set where
22
IsZero (suc _) = False
24
Uncurry : {A : Set}{B : A -> Set} -> ((x : A) -> B x -> Set) -> A × B -> Set
25
Uncurry F p = F (fst p) (snd p)
27
F : (n : Nat) -> IsZero n -> Set
31
f : (p : Nat × IsZero) -> Uncurry F p