[Agda] Associativity of vector concatenation

[Dan Licata]

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