[Agda] non-dependent product

[Florent Balestrieri]

I find the following definition useful in the situation I
want to construct a pair of a non-dependent product without
specifying the result type.

> _′_ : ∀ {A B} → A → B → A × B
> _′_ = _,_

for instance, when defining the following function, if I used
(a , b) ≡ (c , d) instead, it would not be clear what is the
second set of the dependent product type. Agda cannot the
implicit variables.

> pair-≡⟶proj-≡ : ∀ {X Y}
>   {a c : X}
>   {b d : Y}
>   → (a ′ b) ≡ (c ′ d)
>   → a ≡ c × b ≡ d
>
> pair-≡⟶proj-≡
>   = < cong proj₁ , cong proj₂ >

The other possibility is to write:

> (_,_ {B = λ x → Y} a b)

instead of

> (a ′ b)

but I tend to find the latter more readable. Perhaps it is
worth of having this operator in Data.Product.

Cheers
-- Florent