[Agda] Associativity of vector concatenation

[Owen]

Hi,

I'm a complete beginner at Agda, so I tried to type in what I thought would
be the "most natural" way to define an equality for vectors:

data AndEquals : (A : Set) (B : Set) (a : A) (b : B) → Set where
  and-refl : {A : Set} {B : Set} {a : A} {b : B} (fst : A ≡ B) (snd : a ≡
b) → AndEquals A B a b

or, in words, "the types are equal and the terms are equal", where the
"and" is a dependent "and" where the fact that the types are equal can be
used to help express what is meant by "the terms are equal".

This definition of course fails to type-check because `a ≡ b` has operands
of different types. If I could somehow rewrite the type of `b` to be `A` it
could work.

Is the above definition substantially different than heterogeneous equality?

Does anyone have advice for how it could be made to type-check?

Best,
Owen

On Fri, Oct 28, 2016 at 10:23 PM, Dan Licata <drl at cs.cmu.edu> wrote:

> Hi,
>
> Here’s the thread I had in mind from a “few” years ago :)
> https://lists.chalmers.se/pipermail/agda/2008/000153.html
> See in particular Conor’s reply here:
> https://lists.chalmers.se/pipermail/agda/2008/000155.html
> and here:
> https://lists.chalmers.se/pipermail/agda/2008/000159.html
>
> In current Agda (2.5.1.1), it looks like the existential interpretation is
> there: you can prove (even without K) by pattern matching that
>
> data HId {A : Set} (M : A) : {B : Set} → B → Set where
>    HRefl : HId M M
>
> is equivalent to
>
> (p : Id A B) * Id{B} (coe p a) b
>
> See
> https://github.com/dlicata335/hott-agda/blob/master/misc/
> Heterogeneous.agda
> for the main idea (I didn’t wrap with Sigma types).
>
> Note that Id (coe p a) b is equivalent to the inductive family path-over
> type
> PathOver (\X -> X) p a b, but I wanted to keep the file as small as
> possible.
>
> I didn’t include it in the file, but we know that that Sigma-type is
> equivalent to Id{(A : Set) * A} (A,a) (B,a),
> which is the construction Conor uses in his thesis Section 5.1.5 (
> http://strictlypositive.org/thesis.pdf)
> to show that you can get heterogeneous equality from homogeneous equality
> with K.
>
>
> Regarding UIP, it’s also constructed in Conor’s thesis, Sec 5. It’s
> described in the context of
> equality of telescopes, but here’s the special case of telescopes of
> length 1, inspired by that:
>
> Suppose you have heterogeneous equality with, as an elimination rule,
> J for homogeneous instances of heterogeneous equality (i.e. J for HId {A}
> a {A} a’).
> (Note that Agda —without-K helpfully prevents you from proving this, or
> else we’d be in trouble!)
>
> From this, you get that such a homogeneous heterogeneous equality implies
> homogeneous equality
> (without the coercion by an existentially quantified type equality), and
> this will be an equivalence because both types have the same intro and
> elim (refl and J).
> Moving along this equivalence, it suffices to prove UIP for homogeneous
> instances
> of heterogeneous equality.  This follows from
>
>     UIP1' : {A : Set} {x : A} {y : A} (p : HId {A} x {A} y) → HId {HId x
> x} HRefl {HId x y} p
>
> which you can prove because using heterogeneous equality in the result
> gets around
> the usual type checking failure that stops you from proving UIP.  Then the
> y=x case is a
> homogeneous instance of heterogeneous equality, so it can be converted to
> a homogeneous equality.
>
> -Dan
>
> > On Oct 28, 2016, at 2:36 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
> wrote:
> >
> >
> >
> > On 28/10/16 15:59, Dan Licata wrote:
> >>> The idea is very similar to using heterogeneous equality, as you will
> >>> see.
> >>
> >> More precisely, I think that heterogeneous equality (a:A) == (b:B) is
> equivalent to either
> >> (writing PathOver F p a b for your a ≡[ p ] b to make the type family
> explicit,
> >> and writing == for the homogeneous identity type)
> >>
> >> (p : A == B) -> PathOver (\X -> X) p a b
> >>
> >> or
> >>
> >> (p : A == B) * PathOver (\X -> X) p a b
> >>
> >> depending on what the rules for the (a:A) == (b:B) type are
> >> (there was a thread a few years ago about whether this should imply
> A==B or require A==B, but I can’t find it right now).
> >
> > I'd also like to understand this, and also the claim that the
> elimination principle for heterogeneous equality implies K.
> >
> > Martin
> >
>
> _______________________________________________
> 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/20161028/647440ee/attachment-0001.html