# [Agda] another possible without-K problem

Dan Licata drl at cs.cmu.edu
Wed Jul 10 21:38:28 CEST 2013

```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

```