<div dir="ltr"><div>A possible workaround is to define the [Pointed] instance of [Loop^ n A] only for n > 0, for example:<br><br><div style="margin-left:40px">module PointedType where<br><br>open import Data.Nat<br>open import Relation.Binary.PropositionalEquality<br>
<br>record Pointed (A : Set) : Set where<br> field<br> point : A<br><br>open Pointed {{...}}<br><br>Loop : (A : Set) → {{_ : Pointed A}} → Set<br>Loop A {{pointed-A}} = _≡_ {A = A} point point<br><br>Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Set<br>
pointed-Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Pointed (Loop^ (suc n) A)<br><br>Loop^ zero A {{pointed-A}} = A<br>Loop^ (suc zero) A {{pointed-A}} = Loop A<br>Loop^ (suc (suc n)) A {{pointed-A}} = Loop (Loop^ (suc n) A)<br>
where<br> pointed-prev : Pointed (Loop^ (suc n) A)<br> pointed-prev = pointed-Loop^ n A<br><br>pointed-Loop^ zero A = record { point = refl }<br>pointed-Loop^ (suc n) A = record { point = refl }<br><br></div>(I hope my definition of Pointed looks more or less the same as yours) <br>
This is not completely satisfactory because you need an extra clause for Loop^, but it works. <br><br></div>Jesper Cockx<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Oct 1, 2013 at 3:45 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
I’m trying to use instance arguments to implement various things<br>
related to pointed types but I’m facing a problem that I can’t solve.<br>
<br>
A pointed type is a type [A] together with a point [a : A]. I want to<br>
implement pointed types in such a way that by just writing [A], Agda<br>
can guess what the base point is. This is easy to do, just define a<br>
record [Pointed A] with a single field of type [A], and whenever you<br>
need a pointed type [A], add an instance argument of type [Pointed A].<br>
Then you can define terms of type [Pointed A] for various types [A]<br>
and Agda will automatically find the base point when needed.<br>
<br>
Problems arise when I want to define the iterated loop space of a<br>
pointed type [A].<br>
The loop space of a pointed type [A] (called [Loop A]) is the type [a<br>
== a] (propositional equality) where [a] is the base point of [A],<br>
pointed by the reflexivity path.<br>
Then the n-iterated loop space of a pointed type [A] is defined by:<br>
<br>
Loop^ 0 A = A<br>
Loop^ (S n) A = Loop (Loop^ n A)<br>
<br>
It is clear that for all [n] and [A], [Loop^ n A] is pointed because<br>
both [A] and [Loop _] are. But Agda does not guess it automatically,<br>
so we need to prove it simultaneously (this is needed for [Loop (Loop^<br>
n A)] to type check).<br>
<br>
But the problem is that given that [Loop^ 0 A = A], there are now two<br>
different proofs that [A] is pointed, so Agda complains whenever you<br>
want to do anything with [A].<br>
And if [A] is itself a loop space, the problem is even worse.<br>
<br>
This is related to issue 899 (Instance search fails if there are<br>
several definitionally equal values in scope) but also (I think) to<br>
issue 751 (Non-unifiable terms defined by pattern matching are not<br>
detected as such) because I think that Agda would not be able to solve<br>
the metas in the constraint [Loop^ ? ? = A] (which make sense given<br>
that if [A] is a loop space there are several solutions).<br>
<br>
Is it possible to workaround this problem?<br>
Or do you think it would be possible to fix it? I’d be willing to try,<br>
but I don’t know much work this could represent.<br>
<br>
Thanks,<br>
<br>
Guillaume Brunerie<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>