[Agda] non-dependent product

[Nils Anders Danielsson]

On 2009-12-17 15:20, Florent Balestrieri wrote:
>> pair-≡⟶proj-≡ : ∀ {X Y}
>>   {a c : X}
>>   {b d : Y}
>>   → (a ′ b) ≡ (c ′ d)
>>   → a ≡ c × b ≡ d

You could also write the following:

  pair-≡⟶proj-≡ : ∀ {X Y : Set} {a b c d} →
                  _≡_ {A = X × Y} (a , b) (c , d) →
                  a ≡ c × b ≡ d

> Perhaps it is worth of having this operator in Data.Product.

I have added the following operator:

  _,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B
  _,′_ = _,_

(The standard library uses the ′ suffix for non-dependent variants of
functions.)

--
/NAD