<div dir="ltr">On Wed, Jul 10, 2013 at 3:38 PM, Dan Licata <span dir="ltr"><<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I think these examples are OK under my stipulation that<br>
dependent pattern matching works as-is for hset indices.<br>
Nats are an hset, so code with Fin/Vec would be the same as it is in<br>
Agda currently. Does that seem right? There totally could be holes in<br>
it. This was more a stray thought than a well-thought-out proposal.<br>
</blockquote><div><br></div><div> I don't think being an hset is good enough. For instance:<br><br></div><div> data FreeMonoid (A : Set) : Set where<br></div><div> unit : FreeMonoid A<br></div><div> inj : A -> FreeMonoid A<br>
</div><div> mult : (x y : FreeMonoid A) -> FreeMonoid A<br></div><div> ident-l : ∀ y -> mult unit y = y<br></div><div> ident-r : ∀ x -> mult x unit = x<br></div><div> assoc : ∀ x y z -> mult x (mult y z) = mult (mult x y) z<br>
</div><div> k : (x y : FreeMonoid A) -> (p q : x = y) -> p = q<br><br></div><div>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.<br>
<br></div><div>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:<br>
<br></div><div> data T (A : Set) : Set where<br></div><div> t : A -> T A<br></div><div> triv : ∀ x y -> x ≠ y -> t x = t y<br><br></div><div>also looks contractible (I think; it seems like a generalization of the interval), but t is not injective.<br>
<br></div><div>-- Dan<br></div></div></div></div>