[Agda] unsolved metas in Respects₂

[Sergei Meshveliani]

Please,
how to fix the below code?

It defines  StrictTotalOrder  on  A × B,  where the comparison is by the
first component (so that B is a dummy factor).

The  development Agda of November ~20 2013 MAlonzo  
reports of 
          unsolved metas  in the line of  " = (foo1 , foo2)".

I have introduced several intermediate signatures -- to make sure in the
types, and wonder what else is needed to resolve this direct product
expression.

Thanks,

------
Sergei


-------------------------------------------------------------------------
open import Level           using (Level; _⊔_)
open import Function        using (flip; _on_)
open import Relation.Binary using
     (Rel; Reflexive; Symmetric; Transitive; IsEquivalence;
      module IsEquivalence; _Respects_; _Respects₂_; Trichotomous; 
      IsStrictTotalOrder; module IsStrictTotalOrder; StrictTotalOrder;
      module StrictTotalOrder
     )
open import Data.Product using (_×_; _,_; proj₁; proj₂)


stoForPairBy1 : ∀ {α α= α< β} → StrictTotalOrder α α= α< → Set β →
                                        StrictTotalOrder (α ⊔ β) α= α<  
stoForPairBy1 {α} {α=} {α<} {β} stoA B =
                                   record{ Carrier            = A × B
                                         ; _≈_                = _=₁_
                                         ; _<_                = _<₁_
                                         ; isStrictTotalOrder = isSTO₁ }
   where
   open StrictTotalOrder stoA using ()
              renaming (Carrier to A; _≈_ to _=a_; _<_ to _<a_;
                                          isStrictTotalOrder to isSTO-A)
   open IsStrictTotalOrder isSTO-A using ()
              renaming (isEquivalence to aEquiv; trans to <a-trans;
                               compare to aCompare; <-resp-≈ to <a-cong)
   open IsEquivalence aEquiv using ()
                  renaming (refl to aRefl; sym to aSym; trans to aTrans)

   _=₁_ :  Rel (A × B) α=
   _=₁_ =  _=a_ on proj₁

   _<₁_ :  Rel (A × B) α<
   _<₁_ =  _<a_ on proj₁

   =₁refl : Reflexive _=₁_
   =₁refl = aRefl

   =₁sym : Symmetric _=₁_
   =₁sym = aSym

   =₁trans : Transitive _=₁_
   =₁trans = aTrans

   =₁equiv : IsEquivalence _=₁_
   =₁equiv = record{ refl  = \ {x}         → =₁refl {x}
                   ; sym   = \ {x} {y}     → =₁sym {x} {y}
                   ; trans = \ {x} {y} {z} → =₁trans {x} {y} {z} }

   <₁trans : Transitive _<₁_
   <₁trans = <a-trans

   compare₁ : Trichotomous _=₁_ _<₁_
   compare₁ (a , _) (a' , _) =  aCompare a a'

   <a-cong1 : {x : A} → (_<a_ x) Respects _=a_
   <a-cong1 = proj₁ <a-cong

   <a-cong2 : {y : A} → (flip _<a_ y) Respects _=a_
   <a-cong2 = proj₂ <a-cong

   cong-<₁1 : ∀ {p} → (_<₁_ p) Respects _=₁_
   cong-<₁1 {p1 , _} {q1 , _} {q1' , _} q=q' p<q =  <a-cong1 q=q' p<q

   cong-<₁2 : ∀ {q} → (flip _<₁_ q) Respects _=₁_
   cong-<₁2 {q1 , _} {p1 , _} {p1' , _} p=p' p<q =  <a-cong2 p=p' p<q

   cong-<₁ : _<₁_ Respects₂ _=₁_
                         -- {α ⊔ β} {α<} {α=} {A × B} _<₁_ _=₁_         
   cong-<₁ = pp
       where
       foo1 : ∀ {p} → (_<₁_ p) Respects _=₁_
       foo1 {p} {q} {q'}= cong-<₁1 {p} {q} {q'}

       foo2 : ∀ {q} → (flip _<₁_ q) Respects _=₁_
       foo2 {q} {p} {p'} =  cong-<₁2 {q} {p} {p'}

       pp : (∀ {p} → (_<₁_ p) Respects _=₁_) ×
            (∀ {q} → (flip _<₁_ q) Respects _=₁_)
       pp = (foo1 , foo2)

   isSTO₁ : IsStrictTotalOrder _=₁_ _<₁_
   isSTO₁ = record{ isEquivalence = =₁equiv
                  ; trans    = \ {x} {y} {z} → <₁trans {x} {y} {z}
                  ; compare  = compare₁
                  ; <-resp-≈ = cong-<₁ 
                  }