One can easily Church-encode pairs like that:
Definition prod (X Y:Set) : Set := forall (Z : Set), (X -> Y -> Z) -> Z.
Definition pair (X Y:Set)(x:X)(y:Y) : prod X Y := fun Z xy => xy x y.
Definition pair_rec (X Y Z:Set)(p:X->Y->Z) (xy : prod X Y) : Z := xy Z p.
Definition fst (X Y:Set)(xy:prod X Y) : X := pair_rec X Y X (fun x y => x) xy.
Definition snd (X Y:Set)(xy:prod X Y) : Y := pair_rec X Y Y (fun x y => y) xy.
It is then tempting to generalize it to dependent pairs like that:
Definition dprod (X:Set)(Y:X->Set) : Set :=
forall (Z : Set), (forall (x:X),Y x->Z)->Z.
Definition dpair (X:Set)(Y:X->Set)(x:X)(y:Y x) : dprod X Y :=
fun Z xy => xy x y.
Definition dpair_rec (X:Set)(Y:X->Set)(Z:Set)(p:forall (x:X),Y x->Z)
(xy : dprod X Y) : Z := xy Z p.
Definition dfst (X:Set)(Y:X->Set)(xy:dprod X Y) : X :=
dpair_rec X Y X (fun x y => x) xy.
Definition dsnd (X:Set)(Y:X->Set)(xy:dprod X Y) : Y (dfst X Y xy) :=
dpair_rec X Y (Y (dfst X Y xy)) (fun x y => y) xy.
However the last definition fails with the error message:
In environment
X : Set
Y : X -> Set
xy : dprod X Y
x : X
y : Y x
The term "y" has type "Y x"
while it is expected to have type
"Y (dfst X Y xy)".
I understand the problem here. But what is the solution? In other words, how to Church-encode dependent pairs?
First of all, let’s get the terminology right.
What you are calling dprod is actually a “dependent sum”, while a “dependent product” is this thing that you might be tempted to call a “dependent function”. The reason for this is that dependent functions generalise regular products, you only have to cleverly use Bool:
prod : Set -> Set -> Set
prod A B = (b : Bool) -> case b of { True -> A; False -> B; }
{-
The type-theoretic notation would be:
prod A B = Π Bool (\b -> case b of { True -> A; False -> B; })
-}
mkPair : (A B : Set) -> A -> B -> prod A B
mkPair A B x y = \b -> case b of { True -> x; False -> y; }
elimProd : (A B Z : Set) -> (A -> B -> Z) -> prod A B -> Z
elimProd A B Z f p = f (p True) (p False)
In the same spirit, dependent pairs (usually denoted Σ) generalise regular sums:
sum : Set -> Set -> Set
sum A B = Σ Bool (\b -> case b of { True -> A; False -> B; })
mkLeft : (A B : Set) -> A -> sum A B
mkLeft A B x = (True, x)
mkRight : (A B : Set) -> B -> sum A B
mkRight A B y = (False, y)
elimSum : (A B Z : Set) -> (A -> Z) -> (B -> Z) -> sum A B -> Z
elimSum A B Z f _ (True, x) = f x
elimSum A B Z _ g (False, y) = g y
It might be confusing, but, on the other hand, Π A (\_ -> B) is the type of regular functions, while Σ A (\_ -> B) is the type of regular pairs (see, for example, here).
So, once again:
Your question can be rephrased in the following way:
Does there exist a Church-encoding for dependent sums via dependent products?
This has been already asked before on Math.StackExchange, and here is an answer that gives essentially the same encoding as yours.
However, reading the comments to this answer, you will notice that it apparently lacks the expected induction principle. There is also a similar question but regarding Church-encoding for natural numbers, and this answer (in particular the comments) sort of explains why Coq or Agda is not enough to derive the induction principle, you need additional assumptions, such as parametricity. There is yet another similar question on MathOverflow and while the answers do not give a definite “yes” or “no” for the specific case of Agda/Coq, they imply that it is likely impossible.
Lastly, I have to mention, that, as with many other type-theoretic questions nowadays, apparently HoTT is the answer. To quote the beginning of the blog post by Mike Shulman:
In this post I will argue that, improving on previous work of Awodey-Frey-Speight, (higher) inductive types can be defined using impredicative encodings with their full dependent induction principles — in particular, eliminating into all type families without any truncation hypotheses — in ordinary (impredicative) Book HoTT without any further bells or whistles.
(Although the (impredicative) encoding you will get can hardly be called Church encoding.)