blob: 348dd49d93e6f8e6be3f2fa737faafb48c1100fb (
plain)
1
2
3
4
5
6
7
|
Definition UU := Type.
Definition dirprodpair {X Y : UU} := existT (fun x : X => Y).
Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }.
Proof.
refine (dirprodpair _ (fun x => _)).
|