[Agda] Proving equality of pairs

[Brandon Moore]

> I pushed a patch that improves unification so now there is no yellow stuff  
>anymore in the first definition...

I see how that is fixed. I don't understand the example with heterogeneous 
inequality.
I thought i understood why inference does not succeed, but it turns out 
providing
just one of the implicit arguments to _≅_ is sufficient.

Of these three cases in the code far below, only the last has yellow (on the two 
_,_ constructors and on refl).

In each pair the first type argument is easily found to be A, an in each pair 
the
second type argument to Σ gives rise to unification problem, so we have
?B1 A B x1 x2 y1 y2 x1 = B x1
?B2 A B x1 x2 y1 y2 x2 = B x2

The first has solutions ?B1 _ _ _ _ _ _ = B and ?B1 _ _ x1 _ _ _ = (λ _ → B x1)
The second has solutions ?B1 _ _ _ _ _ _ = B and ?B1 _ _ _ x2 _ _ = (λ _ → B x2)

The type arguments to ≅ are then
Σ A (?B1 A B x1 x2 y1 y2)
Σ A (?B2 A B x1 x2 y1 y2)

I don't see how constraining one or the other fixes enough for the
definition to go through.


module Test where

open import Relation.Binary.HeterogeneousEquality
open import Data.Product

product-congr1 :
  (A : Set)(B : A -> Set)(x1 x2 : A)(y1 : B x1)(y2 : B x2)
    -> x1 ≅ x2 -> y1 ≅ y2
    -> _≅_ {A = Σ A B} (x1 , y1) (x2 , y2)
product-congr1 A B x1 .x1 y1 .y1 refl refl = refl

product-congr2 :
  (A : Set)(B : A -> Set)(x1 x2 : A)(y1 : B x1)(y2 : B x2)
    -> x1 ≅ x2 -> y1 ≅ y2
    -> _≅_ (x1 , y1) {B = Σ A B} (x2 , y2)
product-congr2 A B x1 .x1 y1 .y1 refl refl = refl

product-congr :
  (A : Set)(B : A -> Set)(x1 x2 : A)(y1 : B x1)(y2 : B x2)
    -> x1 ≅ x2 -> y1 ≅ y2
    -> (x1 , y1) ≅ (x2 , y2)
product-congr A B x1 .x1 y1 .y1 refl refl = refl