[Agda] unsolved metas in Respects₂

[Twan van Laarhoven]

For some reason Agda becomes happy if you write the implicit arguments:

     pp = (\{p} {x} {y} → cong-<₁1 {p} {x} {y})
        , (\{q} {x} {y} → cong-<₁2 {q} {x} {y})


Twan

On 15/12/13 21:56, Sergei Meshveliani wrote:
> 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-<₁
>                    }
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>