[Agda] Associativity of vector concatenation

[Owen]

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/Het
>> erogeneous.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/737ba41f/attachment.html