[Agda] another possible without-K problem

[Dan Doel]

On Wed, Jul 10, 2013 at 3:38 PM, Dan Licata <drl at cs.cmu.edu> wrote:

> I think these examples are OK under my stipulation that
> dependent pattern matching works as-is for hset indices.
> Nats are an hset, so code with Fin/Vec would be the same as it is in
> Agda currently.  Does that seem right?   There totally could be holes in
> it.  This was more a stray thought than a well-thought-out proposal.
>

 I don't think being an hset is good enough. For instance:

    data FreeMonoid (A : Set) : Set where
      unit : FreeMonoid A
      inj  : A -> FreeMonoid A
      mult : (x y : FreeMonoid A) -> FreeMonoid A
      ident-l : ∀ y -> mult unit y = y
      ident-r : ∀ x -> mult x unit = x
      assoc : ∀ x y z -> mult x (mult y z) = mult (mult x y) z
      k : (x y : FreeMonoid A) -> (p q : x = y) -> p = q

I've discussed this before, and I think Mike Shulman chimed in that this
should be sufficient to define the free monoid over A. We have all the
quotienting out of associativity and unit, and we assert that K holds, so
it's an hset. But, inj and unit are not disjoint from mult, and mult is not
pair-wise injective.

Maybe you meant to say 'has no higher constructors' (if that's the right
term). Which would be more sensible, because I'm not sure how a program is
going ot detect automatically when a higher-inductive definition like the
above is in fact an hset. I'm not really 100% convinced the above is, even,
because I haven't bothered to work through it. But the interval is another
example, which is contractible, but its constructors are not disjoint. And
for instance:

    data T (A : Set) : Set where
      t : A -> T A
      triv : ∀ x y -> x ≠ y -> t x = t y

also looks contractible (I think; it seems like a generalization of the
interval), but t is not injective.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130710/c9c2f2d3/attachment.html