[Agda] Associativity of vector concatenation

[Owen]

Hi Dan,

Ah, thank you. That's very interesting.

Best,
Owen

On Mon, Oct 31, 2016 at 9:25 AM, Dan Licata <drl at cs.cmu.edu> wrote:

> Hi Owen,
>
> I think AndEquals is the same as the Sigma/dependent pair type (p : Id A
> B) * Id{B} (coe p a) b that I was referring to (sorry for the confusion of
> using non-Agda notation).
>
> -Dan
>
> > On Oct 28, 2016, at 11:26 PM, Owen <ellbur at gmail.com> wrote:
> >
> > Hi,
> >
> > I should think for 2 minutes before I hit "send". Of course this works:
> >
> > rewrite-type : (A : Set) (B : Set) (a : A) (eq : A ≡ B) → B
> > rewrite-type A .(A) a refl = a
> >
> > 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
> ≡ (rewrite-type B A b (sym fst))) → AndEquals A B a b
> >
> > I'm still curious whether this is substantially different than
> heterogeneous equality.
> >
> > Best,
> > Owen
> >
> > On Fri, Oct 28, 2016 at 11:21 PM, Owen <ellbur at gmail.com> wrote:
> > 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/20161031/5c5da04c/attachment.html