Pair_Polytype (X:*) (Y:*) : *p = (Data:*) -> (X -> Y -> Data) -> Data
Pair  (X:*) (Y:*) : *m = Monotype (Pair_Polytype X Y)
pair (X:*) (Y:*) (x:X) (y:Y) : Pair X Y
 = monotype (Pair_Polytype X Y)
   (λ(Data:*) (f:X -> Y -> Data) -> f x y)

uncurry (X:*) (Y:*) (Data:*) (r:X -> Y -> Data) (p:Pair X Y) : Data
 = polytype (Pair_Polytype X Y)
   p Data r
curry (X:*) (Y:*) (Data:*) (r:Pair X Y -> Data) (x:X) (y:Y)
 = r (pair X Y x y)

fst (X:*) (Y:*) (p:Pair X Y) : X
 = uncurry X Y X (λ(x:X) (y:Y) -> x) p
snd (X:*) (Y:*) (p:Pair X Y) : Y
 = uncurry X Y Y (λ(x:X) (y:Y) -> y) p
repair (X:*) (Y:*) (p:Pair X Y) : Pair X Y
 = pair X Y (fst X Y p) (snd X Y p)

first (X:*) (Y:*) (Z:*) (f:X -> Z) (p:Pair X Y) : Pair Z Y
 = uncurry X Y (Pair Z Y) (λ(x:X) (y:Y) -> pair Z Y (f x) y) p
second (X:*) (Y:*) (Z:*) (f:Y -> Z) (p:Pair X Y) : Pair X Z
 = uncurry X Y (Pair X Z) (λ(x:X) (y:Y) -> pair X Z x (f y)) p