`{A : X -> Type} `{B : X -> Type} : (forall x, A x) * (forall x, B x) -> (forall x, A x * B x) := fun fg x => (fst fg x, snd fg x).
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.