Library FunctionProduct

Require Export SwapExercise.

Set Implicit Arguments.

Generalizable All Variables.

Local Open Scope type_scope.
Local Open Scope product_scope.

Section function_prod.
If A × B and A' × B' exist, then we can build a function from A × B to A' × B'

  Definition function_prod A A' B B' `(product_type A' B') (f : AA') (g : BB') : A × BA' × B'
    := fun xf (π1 x) × g (π2 x).
End function_prod.