[Agda] unsolved metas in Respects₂
Sergei Meshveliani
mechvel at botik.ru
Mon Dec 16 16:38:21 CET 2013
Thank you.
Earlier, I tried a similar thing. But it was
( \ {p} {x} {y} → cong-<₁1 {p} {x} {y} ,
\ {q} {x} {y} → cong-<₁2 {q} {x} {y}
)
, and it was not type-checked.
------
Sergei
On Mon, 2013-12-16 at 16:01 +0100, Twan van Laarhoven wrote:
> 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
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list