[Agda] another possible without-K problem

[Dan Licata]

On Jul10, Dan Doel wrote:
> (If I'm not mistaken) way back in Eliminating Dependent Pattern Matching
> (at least), it is remarked that the translation relies on both K (or, an
> appropriate heterogeneous equality) and disjointness and injectivity of
> constructors. So it would not be a surprise that removing K does not remove
> disjointness of constructors.

At least for simple types like the natural numbers and booleans, I am
pretty sure that injectivity and disjointness can be proved from J and
large elims.  So I agree that, in a theory with J + large elims but
without K, one can prove disjointness and injectivity.  The question is
whether we want this to be part of pattern matching on identity types in
general, though. 

> Getting rid of this is a big deal, though. If you just throw it away, then
> I don't think definitions like the following work:
> 
>     zip : {A B : Set} {n : ℕ} -> Vec A n -> Vec B n -> Vec (A × B) n
>     zip [] [] = []
>     zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys
> 
> The ability to elide the two other cases relies on the fact that they cause
> unification errors, zero ≠ suc n. But, this presumes disjointness of the
> natural numbers. If we aren't allowed that, then we must write these cases,
> and explicitly appeal to disjointness proofs. Except, Agda (for instance)
> isn't equipped for such a thing; we have no way of accessing a
> propositional 'zero = suc n' in those cases to hand off to a lemma.
> 
> Also, you presumably lose the ability to write things like:
> 
>     foo : ∀ n -> Fin n -> ...
>     foo zero () ...
>     ...
> 
> and similarly have no real recourse for that case in Agda.

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.  

-Dan