[Agda] Using instance arguments for pointed types

[Jesper Cockx]

A possible workaround is to define the [Pointed] instance of [Loop^ n A]
only for n > 0, for example:

module PointedType where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

record Pointed (A : Set) : Set where
  field
    point : A

open Pointed {{...}}

Loop : (A : Set) → {{_ : Pointed A}} → Set
Loop A {{pointed-A}} = _≡_ {A = A} point point

Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Set
pointed-Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Pointed (Loop^ (suc
n) A)

Loop^ zero A {{pointed-A}} = A
Loop^ (suc zero) A {{pointed-A}} = Loop A
Loop^ (suc (suc n)) A {{pointed-A}} = Loop (Loop^ (suc n) A)
  where
    pointed-prev : Pointed (Loop^ (suc n) A)
    pointed-prev = pointed-Loop^ n A

pointed-Loop^ zero    A = record { point = refl }
pointed-Loop^ (suc n) A = record { point = refl }

(I hope my definition of Pointed looks more or less the same as yours)
This is not completely satisfactory because you need an extra clause for
Loop^, but it works.

Jesper Cockx


On Tue, Oct 1, 2013 at 3:45 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> Hi all,
>
> I’m trying to use instance arguments to implement various things
> related to pointed types but I’m facing a problem that I can’t solve.
>
> A pointed type is a type [A] together with a point [a : A]. I want to
> implement pointed types in such a way that by just writing [A], Agda
> can guess what the base point is. This is easy to do, just define a
> record [Pointed A] with a single field of type [A], and whenever you
> need a pointed type [A], add an instance argument of type [Pointed A].
> Then you can define terms of type [Pointed A] for various types [A]
> and Agda will automatically find the base point when needed.
>
> Problems arise when I want to define the iterated loop space of a
> pointed type [A].
> The loop space of a pointed type [A] (called [Loop A]) is the type [a
> == a] (propositional equality) where [a] is the base point of [A],
> pointed by the reflexivity path.
> Then the n-iterated loop space of a pointed type [A] is defined by:
>
>     Loop^ 0 A = A
>     Loop^ (S n) A = Loop (Loop^ n A)
>
> It is clear that for all [n] and [A], [Loop^ n A] is pointed because
> both [A] and [Loop _] are. But Agda does not guess it automatically,
> so we need to prove it simultaneously (this is needed for [Loop (Loop^
> n A)] to type check).
>
> But the problem is that given that [Loop^ 0 A = A], there are now two
> different proofs that [A] is pointed, so Agda complains whenever you
> want to do anything with [A].
> And if [A] is itself a loop space, the problem is even worse.
>
> This is related to issue 899 (Instance search fails if there are
> several definitionally equal values in scope) but also (I think) to
> issue 751 (Non-unifiable terms defined by pattern matching are not
> detected as such) because I think that Agda would not be able to solve
> the metas in the constraint [Loop^ ? ? = A] (which make sense given
> that if [A] is a loop space there are several solutions).
>
> Is it possible to workaround this problem?
> Or do you think it would be possible to fix it? I’d be willing to try,
> but I don’t know much work this could represent.
>
> Thanks,
>
> Guillaume Brunerie
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131001/bb691896/attachment.html